set A = the V5() ManySortedSet of the carrier of S;
take the V5() ManySortedSet of the carrier of S ; :: thesis: the V5() ManySortedSet of the carrier of S is with_missing_variables
thus the V5() ManySortedSet of the carrier of S is with_missing_variables ; :: thesis: verum