let L be complete Scott TopLattice; :: thesis: for VV being Subset of (InclPoset (sigma L))
for X being filtered Subset of L st VV = { ((downarrow x) `) where x is Element of L : x in X } holds
VV is directed
let VV be Subset of (InclPoset (sigma L)); :: thesis: for X being filtered Subset of L st VV = { ((downarrow x) `) where x is Element of L : x in X } holds
VV is directed
let V be filtered Subset of L; :: thesis: ( VV = { ((downarrow x) `) where x is Element of L : x in V } implies VV is directed )
set F = { (downarrow u) where u is Element of L : u in V } ;
{ (downarrow u) where u is Element of L : u in V } c= bool the carrier of L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (downarrow u) where u is Element of L : u in V } or x in bool the carrier of L )
assume x in { (downarrow u) where u is Element of L : u in V } ; :: thesis: x in bool the carrier of L
then ex u being Element of L st
( x = downarrow u & u in V ) ;
hence x in bool the carrier of L ; :: thesis: verum

end;

then reconsider F = { (downarrow u) where u is Element of L : u in V } as Subset-Family of L ;
reconsider F = F as Subset-Family of L ;
assume A1: VV = { ((downarrow x) `) where x is Element of L : x in V } ; :: thesis: VV is directed
VV c= bool the carrier of L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in VV or x in bool the carrier of L )
assume x in VV ; :: thesis: x in bool the carrier of L
then ex u being Element of L st
( x = (downarrow u) ` & u in V ) by A1;
hence x in bool the carrier of L ; :: thesis: verum

end;

then reconsider VV = VV as Subset-Family of L ;
reconsider VV = VV as Subset-Family of L ;

now :: thesis: for x being object holds
( ( x in VV implies x in COMPLEMENT F ) & ( x in COMPLEMENT F implies x in VV ) )

let x be object ; :: thesis: ( ( x in VV implies x in COMPLEMENT F ) & ( x in COMPLEMENT F implies x in VV ) )

hereby :: thesis: ( x in COMPLEMENT F implies x in VV )

assume x in VV ; :: thesis: x in COMPLEMENT F
then consider u being Element of L such that
A2: x = (downarrow u) ` and
A3: u in V by A1;
downarrow u in F by A3;
hence x in COMPLEMENT F by A2, YELLOW_8:5; :: thesis: verum

end;

assume A4: x in COMPLEMENT F ; :: thesis: x in VV
then reconsider X = x as Subset of L ;
X ` in F by A4, SETFAM_1:def 7;
then consider u being Element of L such that
A5: X ` = downarrow u and
A6: u in V ;
X = (downarrow u) ` by A5;
hence x in VV by A1, A6; :: thesis: verum

end;

then VV = COMPLEMENT F by TARSKI:2;
hence VV is directed by Lm2; :: thesis: verum