set x = EmptyMS I;
EmptyMS I c= A by PBOOLE:43;
then reconsider x = EmptyMS I as ManySortedSubset of A by PBOOLE:def 18;
take x ; :: thesis: ( x is V9() & x is V39() )
thus ( x is V9() & x is V39() ) ; :: thesis: verum