theorem Th50: :: YELLOW_9:50
for S, T being non empty reflexive transitive antisymmetric complete Scott TopRelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds
for F being Subset of S
for G being Subset of T st F = G & F is open holds
G is open