let A, B be set ; :: according to FINSUB_1:def 2 :: thesis: ( not A in bool X or not B in bool X or A /\ B in bool X )
assume that
A1: A in bool X and
B in bool X ; :: thesis: A /\ B in bool X
A /\ B c= X by A1, XBOOLE_1:108;
hence A /\ B in bool X ; :: thesis: verum