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

now

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 & ex_sup_of downarrow (sup ({x} "/\" D)),L ) by YELLOW_0:17;
waybelow x c= downarrow (sup ({x} "/\" D))

proof

let q be set ; :: 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 q' being Element of L such that
A3: ( q' = q & q' << x ) ;
A4: q' <= x by A3, WAYBEL_3:1;
consider d being Element of L such that
A5: ( d in D & q' <= d ) by A1, A3, 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 A5;
then A6: x "/\" d in {x} "/\" D by YELLOW_4:def 4;
ex_inf_of {x,d},L by YELLOW_0:17;
then A7: q' <= x "/\" d by A4, A5, YELLOW_0:19;
sup ({x} "/\" D) is_>=_than {x} "/\" D by YELLOW_0:32;
then x "/\" d <= sup ({x} "/\" D) by A6, LATTICE3:def 9;
then q' <= sup ({x} "/\" D) by A7, ORDERS_2:26;
hence q in downarrow (sup ({x} "/\" D)) by A3, WAYBEL_0:17; :: thesis: verum

end;

then sup (waybelow x) <= sup (downarrow (sup ({x} "/\" D))) by A2, YELLOW_0:34;
then sup (waybelow x) <= sup ({x} "/\" D) by WAYBEL_0:34;
then A8: x <= sup ({x} "/\" D) by WAYBEL_3:def 5;
sup ({x} "/\" D) <= x by Lm11;
hence x = sup ({x} "/\" D) by A8, ORDERS_2:25; :: 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