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 or a in Y ) by XBOOLE_0:def 3;
hence contradiction by Def1; :: thesis: verum