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 and
A3: f is Orderinvolutive by OPOSET_1:def 18;
( f is involutive & f is antitone ) by A3, OPOSET_1:def 17;
then f . x >= f . y by A1, WAYBEL_9:def 1;
then x ` >= f . y by A2, ROBBINS1:def 3;
hence y ` <= x ` by A2, ROBBINS1:def 3; :: thesis: verum