let B be Boolean Lattice; :: thesis: for v2, v1, v0 being Element of (BA2TBAA B) holds Tern (v0,v1,v2) = Tern (v0,v2,v1)
let v2, v1, v0 be Element of (BA2TBAA B); :: thesis: Tern (v0,v1,v2) = Tern (v0,v2,v1)
reconsider aa = v0, bb = v1, cc = v2 as Element of B ;
Tern (v0,v1,v2) = Ros (aa,bb,cc) by RosTrnDef
.= Ros (aa,cc,bb) by LATTICES:def 5
.= Tern (v0,v2,v1) by RosTrnDef ;
hence Tern (v0,v1,v2) = Tern (v0,v2,v1) ; :: thesis: verum