let R1, R2 be Subset-Family of S; :: thesis: ( ( for A being Subset of S holds
( A in R1 iff ex B being Subset of T st
( B in G & A = f .: B ) ) ) & ( for A being Subset of S holds
( A in R2 iff ex B being Subset of T st
( B in G & A = f .: B ) ) ) implies R1 = R2 )
assume that
A1: for A being Subset of S holds
( A in R1 iff ex B being Subset of T st
( B in G & A = f .: B ) ) and
A2: for A being Subset of S holds
( A in R2 iff ex B being Subset of T st
( B in G & A = f .: B ) ) ; :: thesis: R1 = R2
for x being set holds
( x in R1 iff x in R2 )

proof

let x be set ; :: thesis: ( x in R1 iff x in R2 )
thus ( x in R1 implies x in R2 ) :: thesis: ( x in R2 implies x in R1 )

proof

assume A3: x in R1 ; :: thesis: x in R2
then reconsider x = x as Subset of S ;
ex B being Subset of T st
( B in G & x = f .: B ) by A1, A3;
hence x in R2 by A2; :: thesis: verum

end;

assume A4: x in R2 ; :: thesis: x in R1
then reconsider x = x as Subset of S ;
ex B being Subset of T st
( B in G & x = f .: B ) by A2, A4;
hence x in R1 by A1; :: thesis: verum

end;

hence R1 = R2 by TARSKI:2; :: thesis: verum