let T be Ternary_Boolean_Algebra; :: thesis: for a, b being Element of T holds Tern (a,(b `),b) = a
let a, b be Element of T; :: thesis: Tern (a,(b `),b) = a
Tern (a,(b `),b) = Tern ((Tern (a,b,(b `))),(b `),b) by TRADef
.= Tern ((Tern (a,b,(b `))),(b `),(Tern (a,b,b))) by TRIDef
.= Tern (a,b,(Tern ((b `),(b `),b))) by TDis
.= Tern (a,b,(b `)) by TLIDef
.= a by TRADef ;
hence Tern (a,(b `),b) = a ; :: thesis: verum