let T be continuous complete Lawson TopLattice; :: thesis: for S being non empty full SubRelStr of T st ( for N being net of T st rng the mapping of N c= the carrier of S holds
lim_inf N in the carrier of S ) holds
S is directed-sups-inheriting
let S be non empty full SubRelStr of T; :: thesis: ( ( for N being net of T st rng the mapping of N c= the carrier of S holds
lim_inf N in the carrier of S ) implies S is directed-sups-inheriting )
set X = the carrier of S;
assume A1: for N being net of T st rng the mapping of N c= the carrier of S holds
lim_inf N in the carrier of S ; :: thesis: S is directed-sups-inheriting
let Y be directed Subset of S; :: according to WAYBEL_0:def 4 :: thesis: ( Y = {} or not ex_sup_of Y,T or "\/" (Y,T) in the carrier of S )
assume Y <> {} ; :: thesis: ( not ex_sup_of Y,T or "\/" (Y,T) in the carrier of S )
then reconsider F = Y as non empty directed Subset of T by YELLOW_2:7;
assume ex_sup_of Y,T ; :: thesis: "\/" (Y,T) in the carrier of S
the mapping of (Net-Str F) = id F by Th32;
then A2: rng the mapping of (Net-Str F) = Y ;
lim_inf (Net-Str F) = sup F by WAYBEL17:10;
hence "\/" (Y,T) in the carrier of S by A1, A2; :: thesis: verum