let i be set ; :: according to PBOOLE:def 16 :: thesis: ( not i in I or not (X \/ Y) . i is empty )
A1: Y c= X \/ Y by PBOOLE:16;
assume A2: i in I ; :: thesis: not (X \/ Y) . i is empty
then (X \/ Y) . i = (X . i) \/ (Y . i) by PBOOLE:def 7;
then A3: Y . i c= (X . i) \/ (Y . i) by A1, A2, PBOOLE:def 5;
thus not (X \/ Y) . i is empty by A2, A3, PBOOLE:def 7; :: thesis: verum