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;

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

hence
x in the topology of (ConvergenceSpace (lim_inf-Convergence L2))
by A2, A4; :: thesis: verumfor 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;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