Union the Sorts of (TermAlg S) = S -Terms ( the carrier of S --> NAT) by MSATERM:13;
hence for b₁ being Element of (TermAlg S) holds
( b₁ is Relation-like & b₁ is Function-like ) ; :: thesis: verum