let L be complete LATTICE; :: thesis: for a, b being Element of L st L is continuous & ( for c being Element of L st c << a holds
c <= b ) holds
a <= b
let a, b be Element of L; :: thesis: ( L is continuous & ( for c being Element of L st c << a holds
c <= b ) implies a <= b )
assume that
A1: L is continuous and
A2: for c being Element of L st c << a holds
c <= b ; :: thesis: a <= b

now

let c be Element of L; :: thesis: ( c in waybelow a implies c <= b )
assume c in waybelow a ; :: thesis: c <= b
then c << a by WAYBEL_3:7;
hence c <= b by A2; :: thesis: verum

end;

then waybelow a is_<=_than b by LATTICE3:def 9;
then sup (waybelow a) <= b by YELLOW_0:32;
hence a <= b by A1, WAYBEL_3:def 5; :: thesis: verum