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
for c being Element of L st c in waybelow a holds
c <= b by A2, WAYBEL_3:7;
then waybelow a is_<=_than b ;
then sup (waybelow a) <= b by YELLOW_0:32;
hence a <= b by A1, WAYBEL_3:def 5; :: thesis: verum