set AR = L -waybelow ;
let x, y, z be Element of L; WAYBEL_4:def 5 ( [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
; [(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; verum