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

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