set AR = L -waybelow ;
let x, y, z, u be Element of L; :: according to WAYBEL_4:def 5 :: thesis: ( u <= x & [x,y] in L -waybelow & y <= z implies [u,z] in L -waybelow )
assume ( u <= x & [x,y] in L -waybelow & y <= z ) ; :: thesis: [u,z] in L -waybelow
then ( u <= x & x << y & y <= z ) by Def2;
then u << z by WAYBEL_3:2;
hence [u,z] in L -waybelow by Def2; :: thesis: verum