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 & ex X being Subset of T st
( X = the carrier of S & X is closed ) holds
S is infs-inheriting
let S be non empty full meet-inheriting SubRelStr of T; :: thesis: ( Top T in the carrier of S & ex X being Subset of T st
( X = the carrier of S & X is closed ) implies S is infs-inheriting )
assume A1: Top T in the carrier of S ; :: thesis: ( for X being Subset of T holds
( not X = the carrier of S or not X is closed ) or S is infs-inheriting )
given X being Subset of T such that A2: X = the carrier of S and
A3: X is closed ; :: 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;
set N = F opp+id ;
assume ex_inf_of Y,T ; :: thesis: "/\" (Y,T) in the carrier of S
the mapping of (F opp+id) = id Y by WAYBEL19:27;
then A4: rng the mapping of (F opp+id) = Y ;
Lim (F opp+id) = {(inf F)} by WAYBEL19:43;
then {(inf F)} c= Cl X by A2, A4, Th27, WAYBEL19:26;
then {(inf F)} c= X by A3, PRE_TOPC:22;
hence "/\" (Y,T) in the carrier of S by A2, ZFMISC_1:31; :: thesis: verum

end;

hence S is infs-inheriting by A1, Th16; :: thesis: verum