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

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