let L1, L2 be complete LATTICE; :: thesis: 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; :: thesis: for T2 being Scott TopAugmentation of L2 st L1,L2 are_isomorphic holds
T1,T2 are_homeomorphic
let T2 be Scott TopAugmentation of L2; :: thesis: ( L1,L2 are_isomorphic implies T1,T2 are_homeomorphic )
given h being Function of L1,L2 such that A1: h is isomorphic ; :: according to WAYBEL_1:def 8 :: thesis: 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 ; :: according to T_0TOPSP:def 1 :: thesis: H is being_homeomorphism
thus H is being_homeomorphism by A1, Th4; :: thesis: verum