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

now

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

end;

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

now

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

end;

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