set T = BA2TBAA B;
set ff = RosTrn B;
A1:
for v1, v0 being Element of (BA2TBAA B) holds Tern (v0,v0,v1) = v0
by TLIDef;
A2:
for v2, v1, v0 being Element of (BA2TBAA B) holds Tern (v0,v1,v2) = Tern (v2,v0,v1)
by LemacikA;
A3:
for v2, v1, v0 being Element of (BA2TBAA B) holds Tern (v0,v1,v2) = Tern (v0,v2,v1)
by LemacikB;
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)))
by LemacikC;
hence
BA2TBAA B is ternary-distributive
by TBA1, A1, A2, A3; verum