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)
A1: ( a < b => (b "/\" a) & a < (- (b "/\" a)) => (- b) ) by Lm5, Th19bis;
- (b =-> (b "/\" a)) < - a by Lm6;
hence a <= b =-> (a "/\" b) by A1, Th5, Def8; :: thesis: verum