let T be Ternary_Boolean_Algebra; :: thesis: for a being Element of T holds (a `) ` = a
let a be Element of T; :: thesis: (a `) ` = a
a = Tern (((a `) `),(a `),a) by TLADef
.= (a `) ` by Lemma34 ;
hence (a `) ` = a ; :: thesis: verum