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 & 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 & x in C ) ) ) implies A = B /\ C )
assume A1: for x being Element of E holds
( x in A iff ( x in B & x in C ) ) ; :: thesis: A = B /\ C

now

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 & x in C ) by A1;
hence x in B /\ C by XBOOLE_0:def 4; :: thesis: verum

end;

hence A c= B /\ C by Th7; :: according to XBOOLE_0:def 10 :: thesis: B /\ C c= A

now

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 & x in C ) by XBOOLE_0:def 4;
hence x in A by A1; :: thesis: verum

end;

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