let i be object ; :: according to PBOOLE:def 13 :: thesis: ( not i in I or not (X (\/) Y) . i is empty )
assume A1: i in I ; :: thesis: not (X (\/) Y) . i is empty
then (X (\/) Y) . i = (X . i) \/ (Y . i) by PBOOLE:def 4;
hence not (X (\/) Y) . i is empty by A1; :: thesis: verum