let Y be Subset of X; :: thesis: not Y is with_pair
let x be pair set ; :: according to FACIRC_1:def 2 :: thesis: not x in Y
assume x in Y ; :: thesis: contradiction
hence contradiction by FACIRC_1:def 2; :: thesis: verum