let R be complete LATTICE; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 } ; :: thesis: ( not D is empty & D is directed )
consider j being Element of Z;
"/\" { (Z . k) where k is Element of Z : k >= j } ,R in D by A1;
hence not D is empty ; :: thesis: D is directed
let x, y be Element of R; :: according to WAYBEL_0:def 1 :: thesis: ( not x in D or not y in D or ex b₁ being Element of the carrier of R st
( b₁ in D & x <= b₁ & y <= b₁ ) )
assume x in D ; :: thesis: ( not y in D or ex b₁ being Element of the carrier of R st
( b₁ in D & x <= b₁ & y <= b₁ ) )
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 ; :: thesis: ex b₁ being Element of the carrier of R st
( b₁ in D & x <= b₁ & y <= b₁ )
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 5;
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; :: thesis: ( z in D & x <= z & y <= z )
thus z in D by A1; :: thesis: ( 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 }

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (Z . k) where k is Element of Z : k >= j } or e in { (Z . k) where k is Element of Z : k >= jx } )
assume e in { (Z . k) where k is Element of Z : k >= j } ; :: thesis: e in { (Z . k) where k is Element of Z : k >= jx }
then consider k being Element of Z such that
A6: e = Z . k and
A7: k >= j ;
reconsider k = k as Element of Z ;
k >= jx by A4, A7, YELLOW_0:def 2;
hence e in { (Z . k) where k is Element of Z : k >= jx } by A6; :: thesis: verum

end;

hence x <= z by A2, WAYBEL_7:3; :: thesis: y <= z
{ (Z . k) where k is Element of Z : k >= j } c= { (Z . k) where k is Element of Z : k >= jy }

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (Z . k) where k is Element of Z : k >= j } or e in { (Z . k) where k is Element of Z : k >= jy } )
assume e in { (Z . k) where k is Element of Z : k >= j } ; :: thesis: e in { (Z . k) where k is Element of Z : k >= jy }
then consider k being Element of Z such that
A8: e = Z . k and
A9: k >= j ;
reconsider k = k as Element of Z ;
k >= jy by A5, A9, YELLOW_0:def 2;
hence e in { (Z . k) where k is Element of Z : k >= jy } by A8; :: thesis: verum

end;

hence y <= z by A3, WAYBEL_7:3; :: thesis: verum