let x, y, z be set ; :: thesis: ( not x in dom <*y,z*> or x = 1 or x = 2 )
assume x in dom <*y,z*> ; :: thesis: ( x = 1 or x = 2 )
then x in Seg 2 by FINSEQ_3:29;
hence ( x = 1 or x = 2 ) by FINSEQ_1:4, TARSKI:def 2; :: thesis: verum