theorem Th53: :: YELLOW_9:53
for S being TopStruct ex T being TopExtension of S st
( T is strict & the topology of S is prebasis of T )