let L be RelStr ; :: thesis: for a, b, c being Element of L holds
( ( a is_<=_than {b,c} implies ( a <= b & a <= c ) ) & ( a <= b & a <= c implies a is_<=_than {b,c} ) & ( a is_>=_than {b,c} implies ( b <= a & c <= a ) ) & ( b <= a & c <= a implies a is_>=_than {b,c} ) )
let a, b, c be Element of L; :: thesis: ( ( a is_<=_than {b,c} implies ( a <= b & a <= c ) ) & ( a <= b & a <= c implies a is_<=_than {b,c} ) & ( a is_>=_than {b,c} implies ( b <= a & c <= a ) ) & ( b <= a & c <= a implies a is_>=_than {b,c} ) )
A1: ( b in {b,c} & c in {b,c} ) by TARSKI:def 2;
hence ( a is_<=_than {b,c} implies ( a <= b & a <= c ) ) ; :: thesis: ( ( a <= b & a <= c implies a is_<=_than {b,c} ) & ( a is_>=_than {b,c} implies ( b <= a & c <= a ) ) & ( b <= a & c <= a implies a is_>=_than {b,c} ) )
thus ( a <= b & a <= c implies a is_<=_than {b,c} ) by TARSKI:def 2; :: thesis: ( a is_>=_than {b,c} iff ( b <= a & c <= a ) )
thus ( a is_>=_than {b,c} implies ( a >= b & a >= c ) ) by A1; :: thesis: ( b <= a & c <= a implies a is_>=_than {b,c} )
assume A2: ( a >= b & a >= c ) ; :: thesis: a is_>=_than {b,c}
let c be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not c in {b,c} or c <= a )
thus ( not c in {b,c} or c <= a ) by A2, TARSKI:def 2; :: thesis: verum