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

( 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