let L be non empty reflexive OrthoRelStr ; :: thesis: ( L is trivial implies ( L is OrderInvolutive & L is Pure & L is PartialOrdered ) )
assume L is trivial ; :: thesis: ( L is OrderInvolutive & L is Pure & L is PartialOrdered )
then reconsider L' = L as non empty trivial reflexive OrthoRelStr ;
reconsider f = the Compl of L' as Function of L',L' ;
consider x being set such that
A1: the carrier of L' = {x} by REALSET1:def 4;
f = id {x} by A1, FUNCT_2:66;
then A2: f is dneg by A1, OPOSET_1:20;
for z, y being Element of L' st z <= y holds
f . z >= f . y

proof

let z, y be Element of L'; :: thesis: ( z <= y implies f . z >= f . y )
assume z <= y ; :: thesis: f . z >= f . y
A3: f . z = x by A1, FUNCT_2:65;
f . y = x by A1, FUNCT_2:65;
hence f . z >= f . y by A3, YELLOW_0:def 1; :: thesis: verum

end;

then f is antitone by WAYBEL_9:def 1;
then A4: f is Orderinvolutive by A2, OPOSET_1:def 32;
L' is Dneg by A2, OPOSET_1:def 6;
hence ( L is OrderInvolutive & L is Pure & L is PartialOrdered ) by A4, OPOSET_1:def 26, OPOSET_1:def 33; :: thesis: verum