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);
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 that
A3: x in CF and
A4: y in CF ; :: thesis: ex b₁ being Element of the carrier of (InclPoset (sigma L)) st
( b₁ in CF & x <= b₁ & y <= b₁ )
A5: sigma L = the topology of L by Th23;
then A6: the carrier of (InclPoset (sigma L)) = the topology of L by YELLOW_1:1;
then ( x in sigma L & y in sigma L ) by A5;
then reconsider x9 = x, y9 = y as Subset of L ;
x9 ` in F by A2, A3, SETFAM_1:def 7;
then consider ux being Element of L such that
A7: x9 ` = downarrow ux and
A8: ux in V by A1;
y9 ` in F by A2, A4, SETFAM_1:def 7;
then consider uy being Element of L such that
A9: y9 ` = downarrow uy and
A10: uy in V by A1;
consider uz being Element of L such that
A11: uz in V and
A12: uz <= ux and
A13: uz <= uy by A8, A10, WAYBEL_0:def 2;
(downarrow uz) ` is open by WAYBEL11:12;
then reconsider z = (downarrow uz) ` as Element of (InclPoset (sigma L)) by A6, PRE_TOPC:def 2;
take z ; :: thesis: ( z in CF & x <= z & y <= z )
downarrow uz in F by A1, A11;
hence z in CF by A2, YELLOW_8:5; :: thesis: ( x <= z & y <= z )
downarrow uz c= downarrow uy by A13, WAYBEL_0:21;
then A14: (downarrow uy) ` c= (downarrow uz) ` by SUBSET_1:12;
downarrow uz c= downarrow ux by A12, WAYBEL_0:21;
then (downarrow ux) ` c= (downarrow uz) ` by SUBSET_1:12;
hence ( x <= z & y <= z ) by A7, A9, A14, YELLOW_1:3; :: thesis: verum