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