let a be set ; FACIRC_1:def 3 ( a in dom <*x,y,z*> implies not <*x,y,z*> . a is pair )
assume
a in dom <*x,y,z*>
; not <*x,y,z*> . a is pair
then
<*x,y,z*> . a in rng <*x,y,z*>
by FUNCT_1:def 3;
then
<*x,y,z*> . a in {x,y,z}
by FINSEQ_2:128;
hence
not <*x,y,z*> . a is pair
by ENUMSET1:def 1; verum