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
verumproof
let G,
H be
Subset-Family of
(T | P);
( ( 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 ) )
;
G = H
for
x being
object holds
(
x in G iff
x in H )
proof
let x be
object ;
( x in G iff x in H )
hereby ( x in H implies x in G )
assume A3:
x in G
;
x in Hthen 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;
verum
end;
assume A4:
x in H
;
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;
verum
end;
hence
G = H
by TARSKI:2;
verum
end;