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