let T1, T2 be TopSpace; :: thesis: for T being non empty TopSpace st T is TopExtension of T1 & T is TopExtension of T2 holds
for R being Refinement of T1,T2 holds T is TopExtension of R
let T be non empty TopSpace; :: thesis: ( T is TopExtension of T1 & T is TopExtension of T2 implies for R being Refinement of T1,T2 holds T is TopExtension of R )
assume that
A1: the carrier of T1 = the carrier of T and
A2: the topology of T1 c= the topology of T and
A3: the carrier of T2 = the carrier of T and
A4: the topology of T2 c= the topology of T ; :: according to YELLOW_9:def 5 :: thesis: for R being Refinement of T1,T2 holds T is TopExtension of R
let R be Refinement of T1,T2; :: thesis: T is TopExtension of R
A5: the carrier of R = the carrier of T \/ the carrier of T by A1, A3, YELLOW_9:def 6;
hence the carrier of R = the carrier of T ; :: according to YELLOW_9:def 5 :: thesis: the topology of R c= the topology of T
reconsider S = the topology of T1 \/ the topology of T2 as prebasis of R by YELLOW_9:def 6;
FinMeetCl S is Basis of R by YELLOW_9:23;
then A6: UniCl (FinMeetCl S) = the topology of R by YELLOW_9:22;
S c= the topology of T by A2, A4, XBOOLE_1:8;
then FinMeetCl S c= FinMeetCl the topology of T by A5, CANTOR_1:14;
then the topology of R c= UniCl (FinMeetCl the topology of T) by A5, A6, CANTOR_1:9;
hence the topology of R c= the topology of T by CANTOR_1:7; :: thesis: verum