let x be ManySortedSubset of A; :: thesis: x is V36()
reconsider x9 = x as ManySortedSet of I ;
x9 c= A by PBOOLE:def 18;
hence x is V36() by Th18; :: thesis: verum