let T be continuous complete Lawson TopLattice; :: thesis: for S being non empty full meet-inheriting SubRelStr of T st Top T in the carrier of S & ( 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 infs-inheriting
let S be non empty full meet-inheriting SubRelStr of T; :: thesis: ( Top T in the carrier of S & ( 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 infs-inheriting )
assume A1: Top T in the carrier of S ; :: thesis: ( ex N being net of T st
( rng the mapping of N c= the carrier of S & not lim_inf N in the carrier of S ) or S is infs-inheriting )
set X = the carrier of S;
assume A2: 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 infs-inheriting
S is filtered-infs-inheriting
proof
let Y be filtered Subset of S; :: according to WAYBEL_0:def 3 :: thesis: ( Y = {} or not ex_inf_of Y,T or "/\" (Y,T) in the carrier of S )
assume Y <> {} ; :: thesis: ( not ex_inf_of Y,T or "/\" (Y,T) in the carrier of S )
then reconsider F = Y as non empty filtered Subset of T by YELLOW_2:7;
assume ex_inf_of Y,T ; :: thesis: "/\" (Y,T) in the carrier of S
the mapping of (F opp+id) = id F by WAYBEL19:27;
then A3: rng the mapping of (F opp+id) = Y ;
lim_inf (F opp+id) = inf F by Th28;
hence "/\" (Y,T) in the carrier of S by A2, A3; :: thesis: verum
end;
hence S is infs-inheriting by A1, Th16; :: thesis: verum