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 A1: a " in A \ B by Th29;
then not a " in B by XBOOLE_0:def 5;
then A2: not a in B "" by Th29;
a in A "" by A1, Th29;
hence a in (A "") \ (B "") by A2, XBOOLE_0:def 5; :: thesis: verum
end;
assume A3: a in (A "") \ (B "") ; :: thesis: a in (A \ B) ""
then not a in B "" by XBOOLE_0:def 5;
then A4: not a " in B by Th29;
a " in A by A3, Th29;
then a " in A \ B by A4, XBOOLE_0:def 5;
hence a in (A \ B) "" by Th29; :: thesis: verum