consider z1 being Element of N such that
A1: ( i <= z1 & i <= z1 ) by YELLOW_6:def 5;
z1 in the carrier of (N | i) by A1, Def7;
hence not N | i is empty ; :: thesis: verum