let z be set ; :: thesis: ( z is pair implies not z is empty )
given x, y being object such that A1: z = [x,y] ; :: according to XTUPLE_0:def 1 :: thesis: not z is empty
thus not z is empty by A1; :: thesis: verum