let L be transitive RelStr ; :: thesis: for x, y being Element of L st x <= y holds
for X being set holds
( ( y is_<=_than X implies x is_<=_than X ) & ( x is_>=_than X implies y is_>=_than X ) )
let x, y be Element of L; :: thesis: ( x <= y implies for X being set holds
( ( y is_<=_than X implies x is_<=_than X ) & ( x is_>=_than X implies y is_>=_than X ) ) )
assume A1: x <= y ; :: thesis: for X being set holds
( ( y is_<=_than X implies x is_<=_than X ) & ( x is_>=_than X implies y is_>=_than X ) )
let X be set ; :: thesis: ( ( y is_<=_than X implies x is_<=_than X ) & ( x is_>=_than X implies y is_>=_than X ) )

hereby :: thesis: ( x is_>=_than X implies y is_>=_than X )

assume A2: y is_<=_than X ; :: thesis: x is_<=_than X
thus x is_<=_than X :: thesis: verum

proof

let z be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not z in X or x <= z )
assume z in X ; :: thesis: x <= z
then z >= y by A2;
hence x <= z by A1, ORDERS_2:3; :: thesis: verum

end;

end;

assume A3: x is_>=_than X ; :: thesis: y is_>=_than X
let z be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not z in X or z <= y )
assume z in X ; :: thesis: z <= y
then x >= z by A3;
hence z <= y by A1, ORDERS_2:3; :: thesis: verum