set y = the Element of IRR F;
assume not IRR F is empty ; :: thesis: contradiction
then the Element of IRR F in IRR F ;
then ex a being Element of F st
( a = the Element of IRR F & a is irreducible ) ;
hence contradiction ; :: thesis: verum