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)
b "/\" a <= a "/\" b ;
then b "/\" a < a "/\" b by Th5;
hence a < b => (a "/\" b) by Def4; :: thesis: verum