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 )
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 ; :: 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 b1 being Element of the carrier of R st
( b1 in D & x <= b1 & y <= b1 ) )
assume x in D ; :: thesis: ( 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 ; :: thesis: 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); :: 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 object ; :: 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:1; :: 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 object ; :: 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:1; :: thesis: verum