let x, y be Element of L; :: according to WAYBEL_4:def 3 :: thesis: ( [x,y] in L -waybelow implies x <= y )
assume [x,y] in L -waybelow ; :: thesis: x <= y
then x << y by Def1;
hence x <= y by WAYBEL_3:1; :: thesis: verum