let L be non empty OrthoLattStr ; :: thesis: ( L is trivial implies ( L is involutive & L is with_Top & L is de_Morgan & L is well-complemented ) )
assume L is trivial ; :: thesis: ( L is involutive & L is with_Top & L is de_Morgan & L is well-complemented )
then reconsider L9 = L as non empty trivial OrthoLattStr ;
A1: for x being Element of L9 holds (x ` ) ` = x by STRUCT_0:def 10;
A2: for x being Element of L9 holds x ` is_a_complement_of x

proof

let x be Element of L9; :: thesis: x ` is_a_complement_of x
A3: ( (x ` ) |_| x = Top L9 & (x ` ) |^| x = Bottom L9 ) by STRUCT_0:def 10;
( x |_| (x ` ) = Top L9 & x |^| (x ` ) = Bottom L9 ) by STRUCT_0:def 10;
hence x ` is_a_complement_of x by A3, LATTICES:def 18; :: thesis: verum

end;

( ( for x, y being Element of L9 holds x |_| (x ` ) = y |_| (y ` ) ) & ( for x, y being Element of L9 holds x |^| y = ((x ` ) |_| (y ` )) ` ) ) by STRUCT_0:def 10;
hence ( L is involutive & L is with_Top & L is de_Morgan & L is well-complemented ) by A1, A2, Def6, Def7, ROBBINS1:def 10, ROBBINS1:def 23; :: thesis: verum