let L1, L2 be complete LATTICE; for T1 being Scott TopAugmentation of L1
for T2 being Scott TopAugmentation of L2 st L1,L2 are_isomorphic holds
T1,T2 are_homeomorphic
let T1 be Scott TopAugmentation of L1; for T2 being Scott TopAugmentation of L2 st L1,L2 are_isomorphic holds
T1,T2 are_homeomorphic
let T2 be Scott TopAugmentation of L2; ( L1,L2 are_isomorphic implies T1,T2 are_homeomorphic )
given h being Function of L1,L2 such that A1:
h is isomorphic
; WAYBEL_1:def 8 T1,T2 are_homeomorphic
A2:
RelStr(# the carrier of L2, the InternalRel of L2 #) = RelStr(# the carrier of T2, the InternalRel of T2 #)
by YELLOW_9:def 4;
RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of T1, the InternalRel of T1 #)
by YELLOW_9:def 4;
then reconsider H = h as Function of T1,T2 by A2;
take
H
; T_0TOPSP:def 1 H is being_homeomorphism
thus
H is being_homeomorphism
by A1, Th4; verum