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