let L be lower-bounded continuous LATTICE; :: thesis: L is meet-continuous

now :: thesis: for D being non empty directed Subset of L
for x being Element of L st x <= sup D holds
x = sup ({x} "/\" D)

let D be non empty directed Subset of L; :: thesis: for x being Element of L st x <= sup D holds
x = sup ({x} "/\" D)
let x be Element of L; :: thesis: ( x <= sup D implies x = sup ({x} "/\" D) )
assume A1: x <= sup D ; :: thesis: x = sup ({x} "/\" D)
A2: ex_sup_of waybelow x,L by YELLOW_0:17;
A3: ex_sup_of downarrow (sup ({x} "/\" D)),L by YELLOW_0:17;
waybelow x c= downarrow (sup ({x} "/\" D))

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in waybelow x or q in downarrow (sup ({x} "/\" D)) )
assume q in waybelow x ; :: thesis: q in downarrow (sup ({x} "/\" D))
then q in { y where y is Element of L : y << x } by WAYBEL_3:def 3;
then consider q9 being Element of L such that
A4: q9 = q and
A5: q9 << x ;
A6: q9 <= x by A5, WAYBEL_3:1;
consider d being Element of L such that
A7: d in D and
A8: q9 <= d by A1, A5, WAYBEL_3:def 1;
x in {x} by TARSKI:def 1;
then x "/\" d in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in D ) } by A7;
then A9: x "/\" d in {x} "/\" D by YELLOW_4:def 4;
ex_inf_of {x,d},L by YELLOW_0:17;
then A10: q9 <= x "/\" d by A6, A8, YELLOW_0:19;
sup ({x} "/\" D) is_>=_than {x} "/\" D by YELLOW_0:32;
then x "/\" d <= sup ({x} "/\" D) by A9;
then q9 <= sup ({x} "/\" D) by A10, ORDERS_2:3;
hence q in downarrow (sup ({x} "/\" D)) by A4, WAYBEL_0:17; :: thesis: verum

end;

then sup (waybelow x) <= sup (downarrow (sup ({x} "/\" D))) by A2, A3, YELLOW_0:34;
then sup (waybelow x) <= sup ({x} "/\" D) by WAYBEL_0:34;
then A11: x <= sup ({x} "/\" D) by WAYBEL_3:def 5;
sup ({x} "/\" D) <= x by Lm11;
hence x = sup ({x} "/\" D) by A11, ORDERS_2:2; :: thesis: verum

end;

then for x being Element of L
for D being non empty directed Subset of L st x <= sup D holds
x = sup ({x} "/\" D) ;
hence L is meet-continuous by WAYBEL_2:52; :: thesis: verum