take R = the V6() ManySortedRelation of (Free (S,X)); :: thesis: ( R is NF-var & R is terminating & R is with_UN_property )
thus ( R is NF-var & R is terminating & R is with_UN_property ) ; :: thesis: verum