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