ex z1 being Element of N st
( i <= z1 & i <= z1 ) by YELLOW_6:def 3;
hence not N | i is empty by Def7; :: thesis: verum