let L be continuous LATTICE; :: thesis: for x, y being Element of L holds
( x <= y iff waybelow x c= waybelow y )
let x, y be Element of L; :: thesis: ( x <= y iff waybelow x c= waybelow y )
thus ( x <= y implies waybelow x c= waybelow y ) by Th12; :: thesis: ( waybelow x c= waybelow y implies x <= y )
assume A1: waybelow x c= waybelow y ; :: thesis: x <= y
A2: ex_sup_of waybelow x,L by WAYBEL_0:75;
ex_sup_of waybelow y,L by WAYBEL_0:75;
then sup (waybelow x) <= sup (waybelow y) by A1, A2, YELLOW_0:34;
then x <= sup (waybelow y) by Def5;
hence x <= y by Def5; :: thesis: verum