let i be object ; :: according to PBOOLE:def 13 :: thesis: ( not i in I or not (bool A) . i is empty )
assume A1: i in I ; :: thesis: not (bool A) . i is empty
not bool (A . i) is empty ;
hence not (bool A) . i is empty by A1, Def1; :: thesis: verum