set irr = { z where z is Element of X : z is_/\-irreducible_in X } ;
{ z where z is Element of X : z is_/\-irreducible_in X } c= X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { z where z is Element of X : z is_/\-irreducible_in X } or x in X )
assume x in { z where z is Element of X : z is_/\-irreducible_in X } ; :: thesis: x in X
then ex z being Element of X st
( x = z & z is_/\-irreducible_in X ) ;
hence x in X ; :: thesis: verum
end;
then reconsider irr = { z where z is Element of X : z is_/\-irreducible_in X } as Subset of X ;
take irr ; :: thesis: for x being set holds
( x in irr iff x is_/\-irreducible_in X )
let x be set ; :: thesis: ( x in irr iff x is_/\-irreducible_in X )
hereby :: thesis: ( x is_/\-irreducible_in X implies x in irr )
assume x in irr ; :: thesis: x is_/\-irreducible_in X
then ex z being Element of X st
( x = z & z is_/\-irreducible_in X ) ;
hence x is_/\-irreducible_in X ; :: thesis: verum
end;
assume A1: x is_/\-irreducible_in X ; :: thesis: x in irr
thus x in irr by A1; :: thesis: verum