let T be continuous complete Lawson TopLattice; :: thesis: for S being non empty full meet-inheriting SubRelStr of T
for X being Subset of T st X = the carrier of S & Top T in X holds
( X is closed iff for N being net of T st N is_eventually_in X holds
lim_inf N in X )
let S be non empty full meet-inheriting SubRelStr of T; :: thesis: for X being Subset of T st X = the carrier of S & Top T in X holds
( X is closed iff for N being net of T st N is_eventually_in X holds
lim_inf N in X )
let X be Subset of T; :: thesis: ( X = the carrier of S & Top T in X implies ( X is closed iff for N being net of T st N is_eventually_in X holds
lim_inf N in X ) )
assume that
A1: X = the carrier of S and
A2: Top T in X ; :: thesis: ( X is closed iff for N being net of T st N is_eventually_in X holds
lim_inf N in X )
hereby :: thesis: ( ( for N being net of T st N is_eventually_in X holds
lim_inf N in X ) implies X is closed )
assume X is closed ; :: thesis: for N being net of T st N is_eventually_in X holds
lim_inf N in X
then S is non empty full infs-inheriting directed-sups-inheriting SubRelStr of T by A1, A2, Th48, Th49;
hence for N being net of T st N is_eventually_in X holds
lim_inf N in X by A1, Th51; :: thesis: verum
end;
assume for N being net of T st N is_eventually_in X holds
lim_inf N in X ; :: thesis: X is closed
then 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 by A1, Th27;
then ( S is infs-inheriting & S is directed-sups-inheriting ) by A1, A2, Th52, Th53;
then ex X being Subset of T st
( X = the carrier of S & X is closed ) by Th50;
hence X is closed by A1; :: thesis: verum