let a be pair set ; :: according to FACIRC_1:def 2 :: thesis: not a in {x,y,z}
assume a in {x,y,z} ; :: thesis: contradiction
hence contradiction by ENUMSET1:def 1; :: thesis: verum