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