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

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