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

proof

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;

then reconsider Y = Y as Subset-Family of T2 by XBOOLE_1:1;
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