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 )
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 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 5;
consider j' being Element of Z such that
A6: ( j' >= j & j' >= j ) by YELLOW_6:def 5;
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 . j' 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 Ex' = { H1(k) where k is Element of Z : S1[k] } as non empty Subset of R by A7, A10;
reconsider Ey' = { H1(k) where k is Element of Z : S2[k] } as non empty Subset of R by A8, A11;
reconsider E' = { H1(k) where k is Element of Z : S3[k] } as non empty Subset of R by A9, A12;
A13: ( ex_inf_of E',R & ex_inf_of Ex',R & ex_inf_of Ey',R ) by WAYBEL_0:76;
thus z in D by A1; :: thesis: ( x <= z & y <= z )
E' c= Ex'
proof
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in E' or e in Ex' )
assume e in E' ; :: thesis: e in Ex'
then consider k being Element of Z such that
A14: e = Z . k and
A15: k >= j ;
reconsider k = k as Element of Z ;
k >= jx by A4, A15, YELLOW_0:def 2;
hence e in Ex' by A14; :: thesis: verum
end;
hence x <= z by A2, A13, YELLOW_0:35; :: thesis: y <= z
E' c= Ey'
proof
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in E' or e in Ey' )
assume e in E' ; :: thesis: e in Ey'
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 >= jy by A5, A17, YELLOW_0:def 2;
hence e in Ey' by A16; :: thesis: verum
end;
hence y <= z by A3, A13, YELLOW_0:35; :: thesis: verum