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

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