let R, S, T be TopStruct ; ( R is Refinement of S,T iff TopStruct(# the carrier of R, the topology of R #) is Refinement of S,T )
hereby ( TopStruct(# the carrier of R, the topology of R #) is Refinement of S,T implies R is Refinement of S,T )
assume A1:
R is
Refinement of
S,
T
;
TopStruct(# the carrier of R, the topology of R #) is Refinement of S,Tthen reconsider R1 =
R as
TopSpace ;
the
topology of
S \/ the
topology of
T is
prebasis of
R
by A1, YELLOW_9:def 6;
then A2:
the
topology of
S \/ the
topology of
T is
prebasis of
TopStruct(# the
carrier of
R1, the
topology of
R1 #)
by Th33;
the
carrier of
TopStruct(# the
carrier of
R1, the
topology of
R1 #)
= the
carrier of
S \/ the
carrier of
T
by A1, YELLOW_9:def 6;
hence
TopStruct(# the
carrier of
R, the
topology of
R #) is
Refinement of
S,
T
by A2, YELLOW_9:def 6;
verum
end;
assume A3:
TopStruct(# the carrier of R, the topology of R #) is Refinement of S,T
; R is Refinement of S,T
then reconsider R1 = R as TopSpace by TEX_2:7;
the topology of S \/ the topology of T is prebasis of TopStruct(# the carrier of R, the topology of R #)
by A3, YELLOW_9:def 6;
then A4:
the topology of S \/ the topology of T is prebasis of R1
by Th33;
the carrier of R1 = the carrier of S \/ the carrier of T
by A3, YELLOW_9:def 6;
hence
R is Refinement of S,T
by A4, YELLOW_9:def 6; verum