let L1, L2 be up-complete /\-complete Semilattice; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies the topology of c= the topology of )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis: the topology of c= the topology of
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of or x in the topology of )
A2: the topology of = { V where V is Subset of L2 : for p being Element of L2 st p in V holds
for N being net of L2 st [N,p] in lim_inf-Convergence L2 holds
N is_eventually_in V
}
by YELLOW_6:def 24;
A3: the topology of = { V where V is Subset of L1 : for p being Element of L1 st p in V holds
for N being net of L1 st [N,p] in lim_inf-Convergence L1 holds
N is_eventually_in V
}
by YELLOW_6:def 24;
assume x in the topology of ; :: thesis: x in the topology of
then consider V being Subset of L1 such that
A4: x = V and
A5: for p being Element of L1 st p in V holds
for N being net of L1 st [N,p] in lim_inf-Convergence L1 holds
N is_eventually_in V by A3;
reconsider V2 = V as Subset of L2 by A1;
now :: thesis: for p being Element of L2 st p in V2 holds
for N being net of L2 st [N,p] in lim_inf-Convergence L2 holds
N is_eventually_in V2
let p be Element of L2; :: thesis: ( p in V2 implies for N being net of L2 st [N,p] in lim_inf-Convergence L2 holds
N is_eventually_in V2 )

assume A6: p in V2 ; :: thesis: for N being net of L2 st [N,p] in lim_inf-Convergence L2 holds
N is_eventually_in V2

let N be net of L2; :: thesis: ( [N,p] in lim_inf-Convergence L2 implies N is_eventually_in V2 )
assume [N,p] in lim_inf-Convergence L2 ; :: thesis:
then ex N1 being strict net of L1 st
( [N1,p] in lim_inf-Convergence L1 & RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of N1, the InternalRel of N1 #) & the mapping of N = the mapping of N1 ) by ;
hence N is_eventually_in V2 by A5, A6, Th7; :: thesis: verum
end;
hence x in the topology of by A2, A4; :: thesis: verum