let I be non empty set ; :: thesis: for P being ManySortedSet of
for i being Element of I holds
( not {P} . i is empty & {P} . i is trivial )
let P be ManySortedSet of ; :: thesis: for i being Element of I holds
( not {P} . i is empty & {P} . i is trivial )
let i be Element of I; :: thesis: ( not {P} . i is empty & {P} . i is trivial )
{P} . i = {(P . i)} by PZFMISC1:def 1;
hence ( not {P} . i is empty & {P} . i is trivial ) ; :: thesis: verum