let B1, B2 be Subset-Family of X; :: thesis: ( ( for x being Subset of X holds
( x in B1 iff ex b being Element of B st b c= x ) ) & ( for x being Subset of X holds
( x in B2 iff ex b being Element of B st b c= x ) ) implies B1 = B2 )
assume that
A1: for x being Subset of X holds
( x in B1 iff ex b being Element of B st b c= x ) and
A2: for x being Subset of X holds
( x in B2 iff ex b being Element of B st b c= x ) ; :: thesis: B1 = B2
thus B1 c= B2 :: according to XBOOLE_0:def 10 :: thesis: B2 c= B1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B1 or x in B2 )
assume A3: x in B1 ; :: thesis: x in B2
then reconsider x = x as Subset of X ;
ex b being Element of B st b c= x by A1, A3;
hence x in B2 by A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B2 or x in B1 )
assume A4: x in B2 ; :: thesis: x in B1
then reconsider x = x as Subset of X ;
ex b being Element of B st b c= x by A2, A4;
hence x in B1 by A1; :: thesis: verum