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

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