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 () 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 ;
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 ;
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 ;
then ( y = the carrier of T1 or y in FinMeetCl the topology of T2 ) by ;
hence y in the topology of T2 by ; :: 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 ;
hence x in the topology of T2 by ; :: thesis: verum