let E be set ; :: thesis: for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( ( x in B & not x in C ) or ( x in C & not x in B ) ) ) ) holds
A = B \+\ C
let A, B, C be Subset of E; :: thesis: ( ( for x being Element of E holds
( x in A iff ( ( x in B & not x in C ) or ( x in C & not x in B ) ) ) ) implies A = B \+\ C )
assume A1: for x being Element of E holds
( x in A iff ( ( x in B & not x in C ) or ( x in C & not x in B ) ) ) ; :: thesis: A = B \+\ C
now :: thesis: for x being Element of E st x in A holds
x in B \+\ C
let x be Element of E; :: thesis: ( x in A implies x in B \+\ C )
assume x in A ; :: thesis: x in B \+\ C
then ( ( x in B & not x in C ) or ( x in C & not x in B ) ) by A1;
then ( x in B \ C or x in C \ B ) by XBOOLE_0:def 5;
hence x in B \+\ C by XBOOLE_0:def 3; :: thesis: verum
end;
hence A c= B \+\ C by Th2; :: according to XBOOLE_0:def 10 :: thesis: B \+\ C c= A
now :: thesis: for x being Element of E st x in B \+\ C holds
x in A
let x be Element of E; :: thesis: ( x in B \+\ C implies x in A )
assume x in B \+\ C ; :: thesis: x in A
then ( x in B \ C or x in C \ B ) by XBOOLE_0:def 3;
then ( ( x in B & not x in C ) or ( x in C & not x in B ) ) by XBOOLE_0:def 5;
hence x in A by A1; :: thesis: verum
end;
hence B \+\ C c= A by Th2; :: thesis: verum