thus for G, H being Subset-Family of (T | P) st ( for Q being Subset of (T | P) holds
( Q in G iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) ) & ( for Q being Subset of (T | P) holds
( Q in H iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) ) holds
G = H :: thesis: verum

proof

let G, H be Subset-Family of (T | P); :: thesis: ( ( for Q being Subset of (T | P) holds
( Q in G iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) ) & ( for Q being Subset of (T | P) holds
( Q in H iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) ) implies G = H )
assume that
A1: for Q being Subset of (T | P) holds
( Q in G iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) and
A2: for Q being Subset of (T | P) holds
( Q in H iff ex R being Subset of T st
( R in F & R /\ P = Q ) ) ; :: thesis: G = H
for x being set holds
( x in G iff x in H )

proof

let x be set ; :: thesis: ( x in G iff x in H )

hereby :: thesis: ( x in H implies x in G )

assume A3: x in G ; :: thesis: x in H
then reconsider X = x as Subset of (T | P) ;
ex R being Subset of T st
( R in F & R /\ P = X ) by A1, A3;
hence x in H by A2; :: thesis: verum

end;

assume A4: x in H ; :: thesis: x in G
then reconsider X = x as Subset of (T | P) ;
ex R being Subset of T st
( R in F & R /\ P = X ) by A2, A4;
hence x in G by A1; :: thesis: verum

end;

hence G = H by TARSKI:2; :: thesis: verum

end;