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