set A = the non-empty ManySortedSet of the carrier of S;
take the non-empty ManySortedSet of the carrier of S ; :: thesis: the non-empty ManySortedSet of the carrier of S is with_missing_variables
thus the non-empty ManySortedSet of the carrier of S is with_missing_variables ; :: thesis: verum