let L be Nelson_Algebra; :: thesis: for a, b being Element of L holds (- a) "\/" b < a => b
let a, b be Element of L; :: thesis: (- a) "\/" b < a => b
(a => b) "/\" ((- a) "\/" b) = (- a) "\/" b by Th12;
then (- a) "\/" b <= a => b ;
hence (- a) "\/" b < a => b by Th5; :: thesis: verum