let T1, T2 be non empty TopSpace; :: thesis: for B being prebasis of T1 st B c= the topology of T2 & the carrier of T1 in the topology of T2 holds

the topology of T1 c= the topology of T2

let B be prebasis of T1; :: thesis: ( B c= the topology of T2 & the carrier of T1 in the topology of T2 implies the topology of T1 c= the topology of T2 )

assume that

A1: B c= the topology of T2 and

A2: the carrier of T1 in the topology of T2 ; :: thesis: the topology of T1 c= the topology of T2

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of T1 or x in the topology of T2 )

FinMeetCl B is Basis of T1 by YELLOW_9:23;

then A3: the topology of T1 = UniCl (FinMeetCl B) by YELLOW_9:22;

assume x in the topology of T1 ; :: thesis: x in the topology of T2

then consider Y being Subset-Family of T1 such that

A4: Y c= FinMeetCl B and

A5: x = union Y by A3, CANTOR_1:def 1;

A6: Y c= the topology of T2

union Y in UniCl the topology of T2 by A6, CANTOR_1:def 1;

hence x in the topology of T2 by A5, CANTOR_1:6; :: thesis: verum

the topology of T1 c= the topology of T2

let B be prebasis of T1; :: thesis: ( B c= the topology of T2 & the carrier of T1 in the topology of T2 implies the topology of T1 c= the topology of T2 )

assume that

A1: B c= the topology of T2 and

A2: the carrier of T1 in the topology of T2 ; :: thesis: the topology of T1 c= the topology of T2

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of T1 or x in the topology of T2 )

FinMeetCl B is Basis of T1 by YELLOW_9:23;

then A3: the topology of T1 = UniCl (FinMeetCl B) by YELLOW_9:22;

assume x in the topology of T1 ; :: thesis: x in the topology of T2

then consider Y being Subset-Family of T1 such that

A4: Y c= FinMeetCl B and

A5: x = union Y by A3, CANTOR_1:def 1;

A6: Y c= the topology of T2

proof

then reconsider Y = Y as Subset-Family of T2 by XBOOLE_1:1;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in the topology of T2 )

assume y in Y ; :: thesis: y in the topology of T2

then consider Z being Subset-Family of T1 such that

A7: Z c= B and

A8: Z is finite and

A9: y = Intersect Z by A4, CANTOR_1:def 3;

Z c= the topology of T2 by A1, A7;

then reconsider Z9 = Z as Subset-Family of T2 by XBOOLE_1:1;

( y = the carrier of T1 or ( Z9 c= the topology of T2 & y = meet Z9 & meet Z9 = Intersect Z9 ) ) by A1, A7, A9, SETFAM_1:def 9;

then ( y = the carrier of T1 or y in FinMeetCl the topology of T2 ) by A8, CANTOR_1:def 3;

hence y in the topology of T2 by A2, CANTOR_1:5; :: thesis: verum

end;assume y in Y ; :: thesis: y in the topology of T2

then consider Z being Subset-Family of T1 such that

A7: Z c= B and

A8: Z is finite and

A9: y = Intersect Z by A4, CANTOR_1:def 3;

Z c= the topology of T2 by A1, A7;

then reconsider Z9 = Z as Subset-Family of T2 by XBOOLE_1:1;

( y = the carrier of T1 or ( Z9 c= the topology of T2 & y = meet Z9 & meet Z9 = Intersect Z9 ) ) by A1, A7, A9, SETFAM_1:def 9;

then ( y = the carrier of T1 or y in FinMeetCl the topology of T2 ) by A8, CANTOR_1:def 3;

hence y in the topology of T2 by A2, CANTOR_1:5; :: thesis: verum

union Y in UniCl the topology of T2 by A6, CANTOR_1:def 1;

hence x in the topology of T2 by A5, CANTOR_1:6; :: thesis: verum