let L be RelStr ; :: thesis: for a, b being Element of L holds
( ( a is_<=_than {b} implies a <= b ) & ( a <= b implies a is_<=_than {b} ) & ( a is_>=_than {b} implies b <= a ) & ( b <= a implies a is_>=_than {b} ) )
let a, b be Element of L; :: thesis: ( ( a is_<=_than {b} implies a <= b ) & ( a <= b implies a is_<=_than {b} ) & ( a is_>=_than {b} implies b <= a ) & ( b <= a implies a is_>=_than {b} ) )
A1: b in {b} by TARSKI:def 1;
hence ( a is_<=_than {b} implies a <= b ) by LATTICE3:def 8; :: thesis: ( ( a <= b implies a is_<=_than {b} ) & ( a is_>=_than {b} implies b <= a ) & ( b <= a implies a is_>=_than {b} ) )

hereby :: thesis: ( a is_>=_than {b} iff b <= a )

assume A2: a <= b ; :: thesis: a is_<=_than {b}
thus a is_<=_than {b} :: thesis: verum

proof

let c be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not c in {b} or a <= c )
thus ( not c in {b} or a <= c ) by A2, TARSKI:def 1; :: thesis: verum

end;

end;

thus ( a is_>=_than {b} implies a >= b ) by A1, LATTICE3:def 9; :: thesis: ( b <= a implies a is_>=_than {b} )
assume A3: a >= b ; :: thesis: a is_>=_than {b}
let c be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not c in {b} or c <= a )
thus ( not c in {b} or c <= a ) by A3, TARSKI:def 1; :: thesis: verum