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

now

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

end;

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

now

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

end;

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