let S1, S2 be non empty reflexive antisymmetric up-complete TopRelStr ; :: thesis: ( 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 implies S2 is Scott )
assume A1: 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 #) ; :: thesis: ( not S1 is Scott or S2 is Scott )
assume A2: S1 is Scott ; :: thesis: S2 is Scott
let T be Subset of S2; :: according to WAYBEL11:def 4 :: thesis: ( ( not T is open or ( T is inaccessible_by_directed_joins & T is upper ) ) & ( not T is inaccessible_by_directed_joins or not T is upper or T is open ) )
reconsider T1 = T as Subset of S1 by A1;
A3: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) by A1;
thus ( T is open implies ( T is inaccessible & T is upper ) ) :: thesis: ( not T is inaccessible_by_directed_joins or not T is upper or T is open )
proof
assume T is open ; :: thesis: ( T is inaccessible & T is upper )
then T in the topology of S2 ;
then T1 is open by A1;
hence ( T is inaccessible & T is upper ) by A3, A2, WAYBEL_0:25, YELLOW_9:47; :: thesis: verum
end;
thus ( T is inaccessible & T is upper implies T is open ) :: thesis: verum
proof
assume ( T is inaccessible & T is upper ) ; :: thesis: T is open
then ( T1 is inaccessible & T1 is upper ) by A3, WAYBEL_0:25, YELLOW_9:47;
then T1 in the topology of S1 by A2, PRE_TOPC:def 2;
hence T is open by A1; :: thesis: verum
end;