let E be set ; :: thesis: for A, B being Subset of E st ( for x being Element of E holds
( x in A iff not x in B ) ) holds
A = B `
let A, B be Subset of E; :: thesis: ( ( for x being Element of E holds
( x in A iff not x in B ) ) implies A = B ` )
assume A1: for x being Element of E holds
( x in A iff not x in B ) ; :: thesis: A = B `
thus A c= B ` :: according to XBOOLE_0:def 10 :: thesis: B ` c= A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B ` )
assume A2: x in A ; :: thesis: x in B `
reconsider x = x as set by TARSKI:1;
A in bool E by Def1;
then A c= E by ZFMISC_1:def 1;
then x in E by A2;
then x is Element of E by Def1;
then A3: not x in B by A1, A2;
x in E by A2, Lm1;
hence x in B ` by A3, XBOOLE_0:def 5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B ` or x in A )
assume A4: x in B ` ; :: thesis: x in A
reconsider x = x as set by TARSKI:1;
B ` in bool E by Def1;
then B ` c= E by ZFMISC_1:def 1;
then x in E by A4;
then reconsider x = x as Element of E by Def1;
not x in B by A4, XBOOLE_0:def 5;
hence x in A by A1; :: thesis: verum