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