let H, G be Subset-Family of T; :: thesis: ( ( for A being Subset of T holds
( A in H iff ex B being Subset of T st
( A = Der B & B in F ) ) ) & ( for A being Subset of T holds
( A in G iff ex B being Subset of T st
( A = Der B & B in F ) ) ) implies H = G )
defpred S₁[ set ] means ex W being Subset of T st
( $1 = Der W & W in F );
assume that
A1: for Z being Subset of T holds
( Z in H iff S₁[Z] ) and
A2: for X being Subset of T holds
( X in G iff S₁[X] ) ; :: thesis: H = G
H = G

proof

now

let Z be set ; :: thesis: ( Z in H implies Z in G )
assume A3: Z in H ; :: thesis: Z in G
S₁[Z] by A1, A3;
hence Z in G by A2; :: thesis: verum

end;

then A4: H c= G by TARSKI:def 3;

now

let X be set ; :: thesis: ( X in G implies X in H )
assume A5: X in G ; :: thesis: X in H
then reconsider X' = X as Subset of T ;
S₁[X'] by A2, A5;
hence X in H by A1; :: thesis: verum

end;

then G c= H by TARSKI:def 3;
hence H = G by A4, XBOOLE_0:def 10; :: thesis: verum

end;

hence H = G ; :: thesis: verum