let L be Nelson_Algebra; for a, b, c being Element of L st b < c holds
( a "\/" b < a "\/" c & a "/\" b < a "/\" c )
let a, b, c be Element of L; ( b < c implies ( a "\/" b < a "\/" c & a "/\" b < a "/\" c ) )
assume A1:
b < c
; ( a "\/" b < a "\/" c & a "/\" b < a "/\" c )
A2:
a < a "\/" c
by Th7;
c < a "\/" c
by Th7;
then A3:
b < a "\/" c
by A1, Def3;
A4:
a "/\" b < a
by Th6;
a "/\" b < b
by Th6;
then
a "/\" b < c
by A1, Def3;
hence
( a "\/" b < a "\/" c & a "/\" b < a "/\" c )
by A3, A4, Def8, A2, Def7; verum