let T be non empty TBAStruct ; :: thesis: ( T is TBA-like implies T is satisfying_TBA1 )
assume T is TBA-like ; :: thesis: T is satisfying_TBA1
then ( T is ternary-distributive & T is ternary-left-idempotent & T is ternary-right-idempotent & T is ternary-left-absorbing & T is ternary-right-absorbing ) ;
then ( ( for v4, v3, v2, v1, v0 being Element of T holds Tern ((Tern (v0,v1,v2)),v3,(Tern (v0,v1,v4))) = Tern (v0,v1,(Tern (v2,v3,v4))) ) & ( for v1, v0 being Element of T holds Tern (v0,v1,v1) = v1 ) & ( for v1, v0 being Element of T holds Tern (v0,v1,(v1 `)) = v0 ) & ( for v1, v0 being Element of T holds Tern (v0,v0,v1) = v0 ) ) ;
hence T is satisfying_TBA1 by TBALemma; :: thesis: verum