let O be non empty connected Poset; :: thesis: for x, y being Element of O holds
( x > y iff not x <= y )
let x, y be Element of O; :: thesis: ( x > y iff not x <= y )
A1: ( x <= y & y <= x implies x = y ) by YELLOW_0:def 3;
( ( x <= y or x >= y ) & x <= x ) by WAYBEL_0:def 29;
hence ( x > y iff not x <= y ) by A1, ORDERS_2:def 6; :: thesis: verum