let B be Boolean Lattice; :: thesis: for v3, v2, v1, v0 being Element of (BA2TBAA B) holds Tern ((Tern (v0,v1,v2)),v1,v3) = Tern (v0,v1,(Tern (v2,v1,v3)))
let v3, v2, v1, v0 be Element of (BA2TBAA B); :: thesis: Tern ((Tern (v0,v1,v2)),v1,v3) = Tern (v0,v1,(Tern (v2,v1,v3)))
A1: for v2, v1, v0 being Element of (BA2TBAA B) holds Tern (v0,v1,v2) = ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" (v0 "\/" v2)

proof

let v2, v1, v0 be Element of (BA2TBAA B); :: thesis: Tern (v0,v1,v2) = ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" (v0 "\/" v2)
reconsider aa = v0, bb = v1, cc = v2 as Element of B ;
Tern (v0,v1,v2) = Ros (aa,bb,cc) by RosTrnDef
.= ((aa "\/" bb) "/\" (bb "\/" cc)) "/\" (cc "\/" aa) by LATTICES:13
.= ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" (v2 "\/" v0) ;
hence Tern (v0,v1,v2) = ((v0 "\/" v1) "/\" (v1 "\/" v2)) "/\" (v0 "\/" v2) ; :: thesis: verum

end;

A3: ( ( for v0, v2, v1 being Element of (BA2TBAA B) holds v0 "\/" (v1 "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2) ) & ( for v0, v2, v1 being Element of (BA2TBAA B) holds v0 "/\" (v1 "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" v2) ) ) by LemacikD, LemacikE;
( ( for v2, v1, v0 being Element of (BA2TBAA B) holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v2, v1, v0 being Element of (BA2TBAA B) holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) ) by LATTICES:def 5, LATTICES:def 7;
hence Tern ((Tern (v0,v1,v2)),v1,v3) = Tern (v0,v1,(Tern (v2,v1,v3))) by A1, A3, TBA2; :: thesis: verum