let E be non empty set ; :: thesis: for e1, e2 being Singleton of E holds
( e1 = e2 or e1 misses e2 )
let e1, e2 be Singleton of E; :: thesis: ( e1 = e2 or e1 misses e2 )
e1 /\ e2 c= e1 by XBOOLE_1:17;
then ( e1 /\ e2 = {} or e1 /\ e2 = e1 ) by Th1;
then ( e1 c= e2 or e1 /\ e2 = {} ) by XBOOLE_1:17;
hence ( e1 = e2 or e1 misses e2 ) by Th1; :: thesis: verum