let L1, L2 be up-complete /\-complete Semilattice; ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies the topology of (ConvergenceSpace (lim_inf-Convergence L1)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L2)) )
assume A1:
RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #)
; the topology of (ConvergenceSpace (lim_inf-Convergence L1)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L2))
let x be object ; TARSKI:def 3 ( not x in the topology of (ConvergenceSpace (lim_inf-Convergence L1)) or x in the topology of (ConvergenceSpace (lim_inf-Convergence L2)) )
A2:
the topology of (ConvergenceSpace (lim_inf-Convergence L2)) = { 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 (ConvergenceSpace (lim_inf-Convergence L1)) = { 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 (ConvergenceSpace (lim_inf-Convergence L1))
; x in the topology of (ConvergenceSpace (lim_inf-Convergence L2))
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 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 V2let p be
Element of
L2;
( 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
;
for N being net of L2 st [N,p] in lim_inf-Convergence L2 holds
N is_eventually_in V2let N be
net of
L2;
( [N,p] in lim_inf-Convergence L2 implies N is_eventually_in V2 )assume
[N,p] in lim_inf-Convergence L2
;
N is_eventually_in V2then
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 A1, Th6;
hence
N is_eventually_in V2
by A5, A6, Th7;
verum end;
hence
x in the topology of (ConvergenceSpace (lim_inf-Convergence L2))
by A2, A4; verum