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 ) ) by LATTICE3:def 8; :: 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} ) )

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

assume A2: ( a <= b & a <= c ) ; :: thesis: a is_<=_than {b,c}
thus a is_<=_than {b,c} :: thesis: verum

proof

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

end;

end;

thus ( a is_>=_than {b,c} implies ( a >= b & a >= c ) ) by A1, LATTICE3:def 9; :: thesis: ( b <= a & c <= a implies a is_>=_than {b,c} )
assume A3: ( 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 A3, TARSKI:def 2; :: thesis: verum