theorem Th21: :: WAYBEL14:21

for T being non empty TopSpace
for L being TopLattice
for t being Point of T
for l being Point of L
for X being Subset-Family of L st TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of L, the topology of L #) & t = l & X is Basis of l holds
X is Basis of t