consider A being V5 ManySortedSet of the carrier of S;
take A ; :: thesis: A is with_missing_variables
thus A is with_missing_variables ; :: thesis: verum