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