:: deftheorem defines Topology_of OPENLATT:def 1 :
for T being TopStruct holds Topology_of T = the topology of T;