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

proof

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

end;

hence ( L is involutive & L is with_Top & L is de_Morgan & L is well-complemented ) by A1, A2, A3, Def6, Def7, ROBBINS1:def 10, ROBBINS1:def 23; :: thesis: verum