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
for x being object st x in Y holds
x in X by A2, A3;
then A4: Y c= X ;
for x being object st x in X holds
x in Y by A3, A2;
then X c= Y ;
hence X = Y by A4; :: thesis: verum