let L be Nelson_Algebra; :: thesis: for a, b, c, d being Element of L st a < b & c < d holds
( a "\/" c < b "\/" d & a "/\" c < b "/\" d )
let a, b, c, d be Element of L; :: thesis: ( a < b & c < d implies ( a "\/" c < b "\/" d & a "/\" c < b "/\" d ) )
assume ( a < b & c < d ) ; :: thesis: ( a "\/" c < b "\/" d & a "/\" c < b "/\" d )
then ( a "\/" c < a "\/" d & a "/\" c < a "/\" d & a "\/" d < b "\/" d & a "/\" d < b "/\" d ) by Lm1;
hence ( a "\/" c < b "\/" d & a "/\" c < b "/\" d ) by Def3; :: thesis: verum