let i be object ; :: according to PBOOLE:def 12 :: thesis: ( not i in I or (union (EmptyMS I)) . i is empty )
A1: union ((EmptyMS I) . i) is empty by PBOOLE:5, ZFMISC_1:2;
assume i in I ; :: thesis: (union (EmptyMS I)) . i is empty
hence (union (EmptyMS I)) . i is empty by A1, Def2; :: thesis: verum