let T be continuous complete Lawson TopLattice; :: thesis: for S being non empty full infs-inheriting directed-sups-inheriting SubRelStr of T
for N being net of T st N is_eventually_in the carrier of S holds
lim_inf N in the carrier of S
let S be non empty full infs-inheriting directed-sups-inheriting SubRelStr of T; :: thesis: for N being net of T st N is_eventually_in the carrier of S holds
lim_inf N in the carrier of S
set X = the carrier of S;
let N be net of T; :: thesis: ( N is_eventually_in the carrier of S implies lim_inf N in the carrier of S )
assume N is_eventually_in the carrier of S ; :: thesis: lim_inf N in the carrier of S
then consider a being Element of N such that
N . a in the carrier of S and
A1: rng the mapping of (N | a) c= the carrier of S by Th42;
deffunc H₁( Element of (N | a)) -> set = { ((N | a) . i) where i is Element of (N | a) : i >= $1 } ;
reconsider iN = { ("/\" (H₁(j),T)) where j is Element of (N | a) : verum } as non empty directed Subset of T by Th25;
iN c= the carrier of S

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in iN or z in the carrier of S )
assume z in iN ; :: thesis: z in the carrier of S
then consider j being Element of (N | a) such that
A2: z = "/\" (H₁(j),T) ;
H₁(j) c= the carrier of S

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in H₁(j) or u in the carrier of S )
assume u in H₁(j) ; :: thesis: u in the carrier of S
then ex i being Element of (N | a) st
( u = (N | a) . i & i >= j ) ;
then u in rng the mapping of (N | a) by FUNCT_2:4;
hence u in the carrier of S by A1; :: thesis: verum

end;

then reconsider Xj = H₁(j) as Subset of S ;
ex_inf_of Xj,T by YELLOW_0:17;
hence z in the carrier of S by A2, YELLOW_0:def 18; :: thesis: verum

end;

then reconsider jN = iN as non empty Subset of S ;
A3: jN is directed by WAYBEL10:23;
ex_sup_of jN,T by YELLOW_0:17;
then "\/" (jN,T) in the carrier of S by A3, WAYBEL_0:def 4;
then lim_inf (N | a) in the carrier of S by WAYBEL11:def 6;
hence lim_inf N in the carrier of S by Th41; :: thesis: verum