let L be 1 -element OrthoLattStr ; :: thesis: ( L is involutive & L is with_Top & L is de_Morgan & L is well-complemented )
reconsider L9 = L as 1 -element 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 by STRUCT_0:def 10;
( ( 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, ROBBINS1:def 10, ROBBINS1:def 23; :: thesis: verum