let L be Nelson_Algebra; :: thesis: for a, b being Element of L holds a < a "\/" b
let a, b be Element of L; :: thesis: a < a "\/" b
a <= a "\/" b by LATTICES:4, LATTICES:5;
hence a < a "\/" b by Th5; :: thesis: verum