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