let L be Nelson_Algebra; :: thesis: for a, b being Element of L holds
( a <= b iff ( a < b & - b < - a ) )
let a, b be Element of L; :: thesis: ( a <= b iff ( a < b & - b < - a ) )
thus ( a <= b implies ( a < b & - b < - a ) ) :: thesis: ( a < b & - b < - a implies a <= b )
proof
assume a <= b ; :: thesis: ( a < b & - b < - a )
then a =-> b = Top L by Def6;
hence ( a < b & - b < - a ) by Th4; :: thesis: verum
end;
assume ( a < b & - b < - a ) ; :: thesis: a <= b
then a =-> b = Top L ;
hence a <= b by Def6; :: thesis: verum