let z, X, y1, y2 be set ; :: thesis: ( z in [:X,{y1,y2}:] implies ( z `1 in X & ( z `2 = y1 or z `2 = y2 ) ) )
assume A1: z in [:X,{y1,y2}:] ; :: thesis: ( z `1 in X & ( z `2 = y1 or z `2 = y2 ) )
then z `2 in {y1,y2} by Th10;
hence ( z `1 in X & ( z `2 = y1 or z `2 = y2 ) ) by A1, Th10, TARSKI:def 2; :: thesis: verum