consider A being V5() ManySortedSet of ;
take A ; :: thesis: A is with_missing_variables
thus A is with_missing_variables ; :: thesis: verum