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 )

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

thus
( T is inaccessible & T is upper implies T is open )
:: thesis: verum
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;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

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;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