let R1, R2 be Subset-Family of T; ( ( for A being Subset of T holds
( A in R1 iff ex B being Subset of S st
( B in G & A = f " B ) ) ) & ( for A being Subset of T holds
( A in R2 iff ex B being Subset of S st
( B in G & A = f " B ) ) ) implies R1 = R2 )
assume that
A1:
for A being Subset of T holds
( A in R1 iff ex B being Subset of S st
( B in G & A = f " B ) )
and
A2:
for A being Subset of T holds
( A in R2 iff ex B being Subset of S st
( B in G & A = f " B ) )
; R1 = R2
for x being object holds
( x in R1 iff x in R2 )
proof
let x be
object ;
( x in R1 iff x in R2 )
thus
(
x in R1 implies
x in R2 )
( x in R2 implies x in R1 )proof
assume A3:
x in R1
;
x in R2
then reconsider x =
x as
Subset of
T ;
ex
B being
Subset of
S st
(
B in G &
x = f " B )
by A1, A3;
hence
x in R2
by A2;
verum
end;
assume A4:
x in R2
;
x in R1
then reconsider x =
x as
Subset of
T ;
ex
B being
Subset of
S st
(
B in G &
x = f " B )
by A2, A4;
hence
x in R1
by A1;
verum
end;
hence
R1 = R2
by TARSKI:2; verum