:: deftheorem defines Orderinvolutive OPOSET_1:def 17 :
for PO being non empty RelStr
for f being UnOp of the carrier of PO holds
( f is Orderinvolutive iff ( f is V256() & f is antitone ) );