let E be non empty set ; :: thesis: for A, B being Subset of E
for e being El_ev 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 El_ev of E st e = A \/ B & A <> B & not ( A = {} & B = e ) holds
( A = e & B = {} )
let e be El_ev 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 & B c= e ) by A1, XBOOLE_1:7;
then ( ( A = {} or A = e ) & ( B = {} or B = e ) ) by Th1;
hence ( ( A = {} & B = e ) or ( A = e & B = {} ) ) by A2; :: thesis: verum