let X, Y be Subset of L; :: thesis: ( ( for x being Element of L holds
( x in X iff x is irreducible ) ) & ( for x being Element of L holds
( x in Y iff x is irreducible ) ) implies X = Y )
assume that
A2: for x being Element of L holds
( x in X iff x is irreducible ) and
A3: for x being Element of L holds
( x in Y iff x is irreducible ) ; :: thesis: X = Y

now :: thesis: for x being set st x in Y holds
x in X

let x be set ; :: thesis: ( x in Y implies x in X )
assume A4: x in Y ; :: thesis: x in X
then reconsider x1 = x as Element of L ;
x1 is irreducible by A3, A4;
hence x in X by A2; :: thesis: verum

end;

then A5: Y c= X by TARSKI:def 3;

now :: thesis: for x being set st x in X holds
x in Y

let x be set ; :: thesis: ( x in X implies x in Y )
assume A6: x in X ; :: thesis: x in Y
then reconsider x1 = x as Element of L ;
x1 is irreducible by A2, A6;
hence x in Y by A3; :: thesis: verum

end;

then X c= Y by TARSKI:def 3;
hence X = Y by A5, XBOOLE_0:def 10; :: thesis: verum