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