Free (S,X) = FreeMSA X by MSAFREE3:31;
hence for b₁ being Element of Args (o,(Free (S,X))) holds b₁ is DTree-yielding ; :: thesis: verum