let UN be Universe; :: thesis: for x being Element of UN
for y, z being object st x = [y,z] holds
( y is Element of UN & z is Element of UN )
let x be Element of UN; :: thesis: for y, z being object st x = [y,z] holds
( y is Element of UN & z is Element of UN )
let y, z be object ; :: thesis: ( x = [y,z] implies ( y is Element of UN & z is Element of UN ) )
assume A1: x = [y,z] ; :: thesis: ( y is Element of UN & z is Element of UN )
A2: UN is axiom_GU1 ;
( {y} in x & x in UN ) by A1, TARSKI:def 2;
then ( y in {y} & {y} in UN ) by A2, TARSKI:def 1;
hence y is Element of UN by A2; :: thesis: z is Element of UN
( {y,z} in x & x in UN ) by A1, TARSKI:def 2;
then ( z in {y,z} & {y,z} in UN ) by A2, TARSKI:def 2;
hence z is Element of UN by A2; :: thesis: verum