set AR = L -waybelow ;
let x, y, z be Element of L; :: according to WAYBEL_4:def 5 :: 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, Def1;
y << z by A2, Def1;
then x "\/" y << z by A3, WAYBEL_3:3;
hence [(x "\/" y),z] in L -waybelow by Def1; :: thesis: verum