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