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 ) ; :: thesis: ( ( a <= b implies a is_<=_than {b} ) & ( a is_>=_than {b} implies b <= a ) & ( b <= a implies a is_>=_than {b} ) )
thus ( a <= b implies a is_<=_than {b} ) by TARSKI:def 1; :: thesis: ( a is_>=_than {b} iff b <= a )
thus ( a is_>=_than {b} implies a >= b ) by A1; :: thesis: ( b <= a implies a is_>=_than {b} )
assume A2: 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 A2, TARSKI:def 1; :: thesis: verum