let O be non empty PartialOrdered OrderInvolutive OrthoRelStr ; :: thesis: for x, y being Element of O st x <= y holds
y ` <= x `
let x, y be Element of O; :: thesis: ( x <= y implies y ` <= x ` )
assume A1: x <= y ; :: thesis: y ` <= x `
consider f being Function of O,O such that
A2: ( f = the Compl of O & f is Orderinvolutive ) by OPOSET_1:def 33;
consider g being Function of O,O such that
A3: ( g = f & g is dneg & g is antitone ) by A2, OPOSET_1:def 32;
f . x >= f . y by A1, A3, WAYBEL_9:def 1;
then x ` >= f . y by A2, ROBBINS1:def 3;
hence y ` <= x ` by A2, ROBBINS1:def 3; :: thesis: verum