let L be 1 -element reflexive OrthoRelStr ; :: thesis: ( L is OrderInvolutive & L is Pure & L is PartialOrdered )
reconsider L9 = L as 1 -element reflexive OrthoRelStr ;
reconsider f = the Compl of L9 as Function of L9,L9 ;
consider x being object such that
A1: the carrier of L9 = {x} by ZFMISC_1:131;
f = id {x} by A1, FUNCT_2:51;
then A2: f is V300() ;
then A3: L9 is Dneg by OPOSET_1:def 3;
for z, y being Element of L9 st z <= y holds
f . z >= f . y
proof
let z, y be Element of L9; :: thesis: ( z <= y implies f . z >= f . y )
assume z <= y ; :: thesis: f . z >= f . y
( f . z = x & f . y = x ) by A1, FUNCT_2:50;
hence f . z >= f . y by YELLOW_0:def 1; :: thesis: verum
end;
then f is antitone by WAYBEL_9:def 1;
then f is Orderinvolutive by A2, OPOSET_1:def 17;
hence ( L is OrderInvolutive & L is Pure & L is PartialOrdered ) by A3, OPOSET_1:def 15, OPOSET_1:def 18; :: thesis: verum