let A, B be complex-membered set ; :: thesis: (A \ B) "" = (A "" ) \ (B "" )
let a be complex number ; :: 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 Th35;
then ( a " in A & not a " in B ) by XBOOLE_0:def 5;
then ( a in A "" & not a in B "" ) by Th35;
hence a in (A "" ) \ (B "" ) by XBOOLE_0:def 5; :: thesis: verum

end;

assume a in (A "" ) \ (B "" ) ; :: thesis: a in (A \ B) ""
then ( a in A "" & not a in B "" ) by XBOOLE_0:def 5;
then ( a " in A & not a " in B ) by Th35;
then a " in A \ B by XBOOLE_0:def 5;
hence a in (A \ B) "" by Th35; :: thesis: verum