let A, B be set ; :: according to FINSUB_1:def 2 :: thesis: ( not A in {{},X} or not B in {{},X} or A /\ B in {{},X} )
A1: ( ( A = {} or B = {} ) implies A /\ B = {} ) ;
( A = X & B = X implies A /\ B = X ) ;
hence ( not A in {{},X} or not B in {{},X} or A /\ B in {{},X} ) by A1, TARSKI:def 2; :: thesis: verum