let x, y, z, t be set ; :: thesis: ( not x in dom <*y,z,t*> or x = 1 or x = 2 or x = 3 )
assume x in dom <*y,z,t*> ; :: thesis: ( x = 1 or x = 2 or x = 3 )
then x in Seg 3 by FINSEQ_3:30;
hence ( x = 1 or x = 2 or x = 3 ) by ENUMSET1:def 1, FINSEQ_3:1; :: thesis: verum