theorem Th14: :: WAYBEL29:14

for S1, S2 being non empty reflexive antisymmetric up-complete TopRelStr st TopRelStr(# the carrier of S1, the InternalRel of S1, the topology of S1 #) = TopRelStr(# the carrier of S2, the InternalRel of S2, the topology of S2 #) & S1 is Scott holds
S2 is Scott