let E be non empty set ; :: thesis: for A, B being Subset of E
for e being Singleton of E st e = A \/ B & A <> B & not ( A = {} & B = e ) holds
( A = e & B = {} )
let A, B be Subset of E; :: thesis: for e being Singleton of E st e = A \/ B & A <> B & not ( A = {} & B = e ) holds
( A = e & B = {} )
let e be Singleton of E; :: thesis: ( e = A \/ B & A <> B & not ( A = {} & B = e ) implies ( A = e & B = {} ) )
assume that
A1: e = A \/ B and
A2: A <> B ; :: thesis: ( ( A = {} & B = e ) or ( A = e & B = {} ) )
A c= e by A1, XBOOLE_1:7;
then A3: ( A = {} or A = e ) by Th1;
B c= e by A1, XBOOLE_1:7;
hence ( ( A = {} & B = e ) or ( A = e & B = {} ) ) by A2, A3, Th1; :: thesis: verum