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 set ; :: 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)) )
assume A2:
x in the topology of (ConvergenceSpace (lim_inf-Convergence L1))
; :: thesis: x in the topology of (ConvergenceSpace (lim_inf-Convergence L2))
A3:
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 27;
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 27;
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 A2;
reconsider V2 = V as Subset of L2 by A1;
now 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 V2let 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 V2then consider N1 being
strict net of
L1 such that A7:
(
[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;
thus
N is_eventually_in V2
by A5, A6, A7, Th7;
:: thesis: verum end;
hence
x in the topology of (ConvergenceSpace (lim_inf-Convergence L2))
by A3, A4; :: thesis: verum