consider R being strict TopSpace such that
A1: the carrier of R = the carrier of T and
A2: the topology of T is prebasis of R by Lm1;
take R ; :: thesis: ( the carrier of T = the carrier of R & the topology of T c= the topology of R )
thus ( the carrier of T = the carrier of R & the topology of T c= the topology of R ) by A1, A2, TOPS_2:64; :: thesis: verum