let T be continuous complete Lawson TopLattice; :: thesis:
let S be non empty full infs-inheriting directed-sups-inheriting SubRelStr of T; :: thesis:
set X = the carrier of S;
let N be net of T; :: thesis:
assume N is_eventually_in the carrier of S ; :: thesis:
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

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

let u be object ; :: according to TARSKI:def 3 :: thesis:
assume u in H₁(j) ; :: thesis:
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:

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:

end;