let R be complete LATTICE; for Z being net of R
for D being Subset of R st D = { ("/\" ( { (Z . k) where k is Element of Z : k >= j } ,R)) where j is Element of Z : verum } holds
( not D is empty & D is directed )
let Z be net of R; for D being Subset of R st D = { ("/\" ( { (Z . k) where k is Element of Z : k >= j } ,R)) where j is Element of Z : verum } holds
( not D is empty & D is directed )
let D be Subset of R; ( D = { ("/\" ( { (Z . k) where k is Element of Z : k >= j } ,R)) where j is Element of Z : verum } implies ( not D is empty & D is directed ) )
assume A1:
D = { ("/\" ( { (Z . k) where k is Element of Z : k >= j } ,R)) where j is Element of Z : verum }
; ( not D is empty & D is directed )
set j = the Element of Z;
"/\" ( { (Z . k) where k is Element of Z : k >= the Element of Z } ,R) in D
by A1;
hence
not D is empty
; D is directed
let x, y be Element of R; WAYBEL_0:def 1 ( not x in D or not y in D or ex b1 being Element of the carrier of R st
( b1 in D & x <= b1 & y <= b1 ) )
assume
x in D
; ( not y in D or ex b1 being Element of the carrier of R st
( b1 in D & x <= b1 & y <= b1 ) )
then consider jx being Element of Z such that
A2:
x = "/\" ( { (Z . k) where k is Element of Z : k >= jx } ,R)
by A1;
assume
y in D
; ex b1 being Element of the carrier of R st
( b1 in D & x <= b1 & y <= b1 )
then consider jy being Element of Z such that
A3:
y = "/\" ( { (Z . k) where k is Element of Z : k >= jy } ,R)
by A1;
reconsider jx = jx, jy = jy as Element of Z ;
consider j being Element of Z such that
A4:
j >= jx
and
A5:
j >= jy
by YELLOW_6:def 3;
set E1 = { (Z . k) where k is Element of Z : k >= jx } ;
set Ey = { (Z . k) where k is Element of Z : k >= jy } ;
set E = { (Z . k) where k is Element of Z : k >= j } ;
take z = "/\" ( { (Z . k) where k is Element of Z : k >= j } ,R); ( z in D & x <= z & y <= z )
thus
z in D
by A1; ( x <= z & y <= z )
{ (Z . k) where k is Element of Z : k >= j } c= { (Z . k) where k is Element of Z : k >= jx }
hence
x <= z
by A2, WAYBEL_7:1; y <= z
{ (Z . k) where k is Element of Z : k >= j } c= { (Z . k) where k is Element of Z : k >= jy }
hence
y <= z
by A3, WAYBEL_7:1; verum