defpred S₁[ object ] means ex W being Subset of T st
( $1 = Fr W & W in F );
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 = Fr B & B in F ) ) ) & ( for A being Subset of T holds
( A in G iff ex B being Subset of T st
( A = Fr B & B in F ) ) ) implies H = G )
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

now :: thesis: for X being object st X in G holds
X in H

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

end;

then A4: G c= H ;

now :: thesis: for Z being object st Z in H holds
Z in G

let Z be object ; :: 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 ;
hence H = G by A4; :: thesis: verum