let L be complete Scott TopLattice; :: thesis: for V being filtered Subset of L
for F being Subset-Family of L
for CF being Subset of (InclPoset (sigma L)) st F = { (downarrow u) where u is Element of L : u in V } & CF = COMPLEMENT F holds
CF is directed
let V be filtered Subset of L; :: thesis: for F being Subset-Family of L
for CF being Subset of (InclPoset (sigma L)) st F = { (downarrow u) where u is Element of L : u in V } & CF = COMPLEMENT F holds
CF is directed
let F be Subset-Family of L; :: thesis: for CF being Subset of (InclPoset (sigma L)) st F = { (downarrow u) where u is Element of L : u in V } & CF = COMPLEMENT F holds
CF is directed
let CF be Subset of (InclPoset (sigma L)); :: thesis: ( F = { (downarrow u) where u is Element of L : u in V } & CF = COMPLEMENT F implies CF is directed )
assume that
A1: F = { (downarrow u) where u is Element of L : u in V } and
A2: CF = COMPLEMENT F ; :: thesis: CF is directed
set IPs = InclPoset (sigma L);
A3: sigma L = the topology of L by Th23;
then A4: the carrier of (InclPoset (sigma L)) = the topology of L by YELLOW_1:1;
let x, y be Element of (InclPoset (sigma L)); :: according to WAYBEL_0:def 1 :: thesis: ( not x in CF or not y in CF or ex b₁ being Element of the carrier of (InclPoset (sigma L)) st
( b₁ in CF & x <= b₁ & y <= b₁ ) )
assume A5: ( x in CF & y in CF ) ; :: thesis: ex b₁ being Element of the carrier of (InclPoset (sigma L)) st
( b₁ in CF & x <= b₁ & y <= b₁ )
( x in sigma L & y in sigma L ) by A3, A4;
then reconsider x' = x, y' = y as Subset of L ;
x' ` in F by A2, A5, SETFAM_1:def 8;
then consider ux being Element of L such that
A6: ( x' ` = downarrow ux & ux in V ) by A1;
y' ` in F by A2, A5, SETFAM_1:def 8;
then consider uy being Element of L such that
A7: ( y' ` = downarrow uy & uy in V ) by A1;
consider uz being Element of L such that
A8: ( uz in V & uz <= ux & uz <= uy ) by A6, A7, WAYBEL_0:def 2;
(downarrow uz) ` is open by WAYBEL11:12;
then reconsider z = (downarrow uz) ` as Element of (InclPoset (sigma L)) by A4, PRE_TOPC:def 5;
take z ; :: thesis: ( z in CF & x <= z & y <= z )
downarrow uz in F by A1, A8;
hence z in CF by A2, YELLOW_8:14; :: thesis: ( x <= z & y <= z )
( downarrow uz c= downarrow ux & downarrow uz c= downarrow uy ) by A8, WAYBEL_0:21;
then ( (downarrow ux) ` c= (downarrow uz) ` & (downarrow uy) ` c= (downarrow uz) ` ) by SUBSET_1:31;
hence ( x <= z & y <= z ) by A6, A7, YELLOW_1:3; :: thesis: verum