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

end;

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