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