set R = the invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X));
take T = NFAlgebra the invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)); :: thesis: T is struct-invariant
thus T is struct-invariant ; :: thesis: verum