let a be pair set ; :: 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 Def2; :: thesis: verum