theorem elun2 (A B: set) (a: nat): $ a e. B -> a e. A u. B $;
B C_ A u. B -> a e. B -> a e. A u. B
B C_ A u. B
a e. B -> a e. A u. B