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