let R be /\-complete Semilattice; :: 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;
consider j9 being Element of Z such that
A6: j9 >= j and
j9 >= j by YELLOW_6:def 3;
deffunc H1( Element of Z) -> Element of the carrier of R = Z . $1;
defpred S1[ Element of Z] means $1 >= jx;
defpred S2[ Element of Z] means $1 >= jy;
defpred S3[ Element of Z] means $1 >= j;
set Ex = { H1(k) where k is Element of Z : S1[k] } ;
set Ey = { H1(k) where k is Element of Z : S2[k] } ;
set E = { H1(k) where k is Element of Z : S3[k] } ;
A7: Z . j in { H1(k) where k is Element of Z : S1[k] } by A4;
A8: Z . j in { H1(k) where k is Element of Z : S2[k] } by A5;
A9: Z . j9 in { H1(k) where k is Element of Z : S3[k] } by A6;
A10: { H1(k) where k is Element of Z : S1[k] } is Subset of R from DOMAIN_1:sch 8();
 A11: { H1(k) where k is Element of Z : S2[k] } is Subset of R from DOMAIN_1:sch 8();
 A12: { H1(k) where k is Element of Z : S3[k] } is Subset of R from DOMAIN_1:sch 8();
 take z = "/\" ( { (Z . k) where k is Element of Z : k >= j } ,R); :: thesis: ( z in D & x <= z & y <= z )
reconsider Ex9 = { H1(k) where k is Element of Z : S1[k] } as non empty Subset of R by A7, A10;
reconsider Ey9 = { H1(k) where k is Element of Z : S2[k] } as non empty Subset of R by A8, A11;
reconsider E9 = { H1(k) where k is Element of Z : S3[k] } as non empty Subset of R by A9, A12;
A13: ex_inf_of E9,R by WAYBEL_0:76;
A14: ex_inf_of Ex9,R by WAYBEL_0:76;
A15: ex_inf_of Ey9,R by WAYBEL_0:76;
thus z in D by A1; :: thesis: ( x <= z & y <= z )
E9 c= Ex9
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in E9 or e in Ex9 )
assume e in E9 ; :: thesis: e in Ex9
then consider k being Element of Z such that
A16: e = Z . k and
A17: k >= j ;
reconsider k = k as Element of Z ;
k >= jx by A4, A17, YELLOW_0:def 2;
hence e in Ex9 by A16; :: thesis: verum
end;
hence x <= z by A2, A13, A14, YELLOW_0:35; :: thesis: y <= z
E9 c= Ey9
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in E9 or e in Ey9 )
assume e in E9 ; :: thesis: e in Ey9
then consider k being Element of Z such that
A18: e = Z . k and
A19: k >= j ;
reconsider k = k as Element of Z ;
k >= jy by A5, A19, YELLOW_0:def 2;
hence e in Ey9 by A18; :: thesis: verum
end;
hence y <= z by A3, A13, A15, YELLOW_0:35; :: thesis: verum