let R1, R2 be Subset-Family of S; ( ( 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 ) )
; 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 )
assume A4:
x in R2
;
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;
verum
end;
hence
R1 = R2
by TARSKI:2; verum