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 that
A1: [x,z] in L -waybelow and
A2: [y,z] in L -waybelow ; :: thesis: [(x "\/" y),z] in L -waybelow
A3: x << z by A1, Def2;
y << z by A2, Def2;
then x "\/" y << z by A3, WAYBEL_3:3;
hence [(x "\/" y),z] in L -waybelow by Def2; :: thesis: verum