let L be Nelson_Algebra; :: thesis: 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; :: thesis: ( b <= c implies ( a "\/" b <= a "\/" c & a "/\" b <= a "/\" c ) )
assume A1: b <= c ; :: thesis: ( a "\/" b <= a "\/" c & a "/\" b <= a "/\" c )
A2: a "\/" b < a "\/" c

proof

b < c by A1, Th5;
hence a "\/" b < a "\/" c by Lm1; :: thesis: verum

end;

A3: - (a "\/" c) < - (a "\/" b)

proof

- c < - b by A1, Th5;
then (- a) "/\" (- c) < (- a) "/\" (- b) by Lm1;
then - (a "\/" c) < (- a) "/\" (- b) by Th1;
hence - (a "\/" c) < - (a "\/" b) by Th1; :: thesis: verum

end;

A4: a "/\" b < a "/\" c

proof

b < c by A1, Th5;
hence a "/\" b < a "/\" c by Lm1; :: thesis: verum

end;

- (a "/\" c) < - (a "/\" b)

proof

- c < - b by A1, Th5;
then (- a) "\/" (- c) < (- a) "\/" (- b) by Lm1;
then - (a "/\" c) < (- a) "\/" (- b) by Th8;
hence - (a "/\" c) < - (a "/\" b) by Th8; :: thesis: verum

end;

hence ( a "\/" b <= a "\/" c & a "/\" b <= a "/\" c ) by A4, Th5, A2, A3; :: thesis: verum