let T be continuous complete Lawson TopLattice; :: thesis: for S being non empty full SubRelStr of T st ex X being Subset of T st
( X = the carrier of S & X is closed ) holds
S is directed-sups-inheriting
let S be non empty full SubRelStr of T; :: thesis: ( ex X being Subset of T st
( X = the carrier of S & X is closed ) implies S is directed-sups-inheriting )
given X being Subset of T such that A1: X = the carrier of S and
A2: X is closed ; :: 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 D = Y as non empty directed Subset of T by YELLOW_2:7;
set N = Net-Str D;
assume ex_sup_of Y,T ; :: thesis: "\/" (Y,T) in the carrier of S
the mapping of (Net-Str D) = id Y by Th32;
then rng the mapping of (Net-Str D) = Y ;
then Lim (Net-Str D) c= Cl X by A1, Th27, WAYBEL19:26;
then A3: Lim (Net-Str D) c= X by A2, PRE_TOPC:22;
sup D in Lim (Net-Str D) by Th35;
hence "\/" (Y,T) in the carrier of S by A1, A3; :: thesis: verum