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 (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 #) ; :: thesis: the topology of (ConvergenceSpace (lim_inf-Convergence L1)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L2))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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)) ; :: thesis: 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 :: 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: N is_eventually_in V2
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 A1, Th6;
hence N is_eventually_in V2 by A5, A6, Th7; :: thesis: verum

end;

hence x in the topology of (ConvergenceSpace (lim_inf-Convergence L2)) by A2, A4; :: thesis: verum