let X1 be non empty set ; :: thesis: for A1, B1 being Subset of X1 holds A1 \+\ B1 = { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) }
let A1, B1 be Subset of X1; :: thesis: A1 \+\ B1 = { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) }
thus A1 \+\ B1 c= { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) } :: according to XBOOLE_0:def 10 :: thesis: { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) } c= A1 \+\ B1
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A1 \+\ B1 or a in { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) } )
assume A1: a in A1 \+\ B1 ; :: thesis: a in { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) }
then reconsider x = a as Element of X1 ;
( ( x in A1 & not x in B1 ) or ( not x in A1 & x in B1 ) ) by A1, XBOOLE_0:1;
hence a in { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) } ; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) } or a in A1 \+\ B1 )
assume a in { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) } ; :: thesis: a in A1 \+\ B1
then ex x1 being Element of X1 st
( a = x1 & ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) ) ;
hence a in A1 \+\ B1 by XBOOLE_0:1; :: thesis: verum