let L be Nelson_Algebra; :: thesis: for a, b being Element of L holds
( ( a <= b & b <= a ) iff a = b )
let a, b be Element of L; :: thesis: ( ( a <= b & b <= a ) iff a = b )
thus ( a <= b & b <= a implies a = b ) :: thesis: ( a = b implies ( a <= b & b <= a ) )

proof

assume ( a <= b & b <= a ) ; :: thesis: a = b
then ( a [= b & b [= a ) by LATTICES:4;
hence a = b by LATTICES:8; :: thesis: verum

end;

thus ( a = b implies ( a <= b & b <= a ) ) ; :: thesis: verum