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 L' = L as non empty trivial OrthoLattStr ;
A1: for x being Element of holds (x ` ) ` = x by STRUCT_0:def 10;
A2: for x being Element of holds x ` is_a_complement_of x

proof

let x be Element of ; :: thesis: x ` is_a_complement_of x
A3: ( (x ` ) |_| x = Top L' & (x ` ) |^| x = Bottom L' ) by STRUCT_0:def 10;
( x |_| (x ` ) = Top L' & x |^| (x ` ) = Bottom L' ) 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 holds x |_| (x ` ) = y |_| (y ` ) ) & ( for x, y being Element of 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