let E be non empty set ; :: thesis: for A, B being Subset of E
for e being El_ev of E holds
( not e = A \/ B or ( A = e & B = e ) or ( A = e & B = {} ) or ( A = {} & B = e ) )
let A, B be Subset of E; :: thesis: for e being El_ev of E holds
( not e = A \/ B or ( A = e & B = e ) or ( A = e & B = {} ) or ( A = {} & B = e ) )
let e be El_ev of E; :: thesis: ( not e = A \/ B or ( A = e & B = e ) or ( A = e & B = {} ) or ( A = {} & B = e ) )
assume A1: e = A \/ B ; :: thesis: ( ( A = e & B = e ) or ( A = e & B = {} ) or ( A = {} & B = e ) )
then ( A c= e & B c= e ) by XBOOLE_1:7;
then ( ( A = {} & B = e ) or ( A = e & B = {} ) or ( A = e & B = e ) or ( A = {} & B = {} ) ) by Th1;
hence ( ( A = e & B = e ) or ( A = e & B = {} ) or ( A = {} & B = e ) ) by A1; :: thesis: verum