let a be pair object ; :: according to FACIRC_1:def 2 :: thesis: not a in X /\ Y

assume a in X /\ Y ; :: thesis: contradiction

then a in X by XBOOLE_0:def 4;

hence contradiction by Def1; :: thesis: verum

assume a in X /\ Y ; :: thesis: contradiction

then a in X by XBOOLE_0:def 4;

hence contradiction by Def1; :: thesis: verum