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 L9 = L as non empty trivial reflexive OrthoRelStr ;
reconsider f = the Compl of L9 as Function of L9,L9 ;
consider x being set such that
A1: the carrier of L9 = {x} by REALSET1:def 4;
f = id {x} by A1, FUNCT_2:66;
then A2: f is dneg by A1, OPOSET_1:20;
then A3: L9 is Dneg by OPOSET_1:def 6;
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:65;
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 32;
hence ( L is OrderInvolutive & L is Pure & L is PartialOrdered ) by A3, OPOSET_1:def 26, OPOSET_1:def 33; :: thesis: verum