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 ) ) ) 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 ) ) ) implies A = B \ C )
assume A1: for x being Element of E holds
( x in A iff ( x in B & not x in C ) ) ; :: 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 ) by A1;
hence x in B \ C by XBOOLE_0:def 5; :: 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 & not x in C ) by XBOOLE_0:def 5;
hence x in A by A1; :: thesis: verum

end;

hence B \ C c= A by Th2; :: thesis: verum