let T be continuous complete Lawson TopLattice; 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; ( 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
; ( 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
; S is infs-inheriting
S is filtered-infs-inheriting
proof
let Y be
filtered Subset of
S;
WAYBEL_0:def 3 ( Y = {} or not ex_inf_of Y,T or "/\" (Y,T) in the carrier of S )
assume
Y <> {}
;
( 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
;
"/\" (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;
verum
end;
hence
S is infs-inheriting
by A1, Th16; verum