let A, B be complex-membered set ; :: thesis: (A \/ B) "" = (A "") \/ (B "")
let a be Complex; :: according to MEMBERED:def 13 :: thesis: ( ( not a in (A \/ B) "" or a in (A "") \/ (B "") ) & ( not a in (A "") \/ (B "") or a in (A \/ B) "" ) )
hereby :: thesis: ( not a in (A "") \/ (B "") or a in (A \/ B) "" )
assume a in (A \/ B) "" ; :: thesis: a in (A "") \/ (B "")
then a " in A \/ B by Th29;
then ( a " in A or a " in B ) by XBOOLE_0:def 3;
then ( a in A "" or a in B "" ) by Th29;
hence a in (A "") \/ (B "") by XBOOLE_0:def 3; :: thesis: verum
end;
assume a in (A "") \/ (B "") ; :: thesis: a in (A \/ B) ""
then ( a in A "" or a in B "" ) by XBOOLE_0:def 3;
then ( a " in A or a " in B ) by Th29;
then a " in A \/ B by XBOOLE_0:def 3;
hence a in (A \/ B) "" by Th29; :: thesis: verum