theorem :: ZFMISC_1:86

for X, Y being set holds [:X,Y:] c= bool (bool (X \/ Y))