defpred S_{1}[ Element of L] means $1 is irreducible ;

consider X being Subset of L such that

A1: for x being Element of L holds

( x in X iff S_{1}[x] )
from SUBSET_1:sch 3();

take X ; :: thesis: for x being Element of L holds

( x in X iff x is irreducible )

thus for x being Element of L holds

( x in X iff x is irreducible ) by A1; :: thesis: verum

consider X being Subset of L such that

A1: for x being Element of L holds

( x in X iff S

take X ; :: thesis: for x being Element of L holds

( x in X iff x is irreducible )

thus for x being Element of L holds

( x in X iff x is irreducible ) by A1; :: thesis: verum