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

now

let x1 be set ; :: thesis: ( ( x1 in S1 implies x1 in S2 ) & ( x1 in S2 implies x1 in S1 ) )
thus ( x1 in S1 implies x1 in S2 ) :: thesis: ( x1 in S2 implies x1 in S1 )

proof

assume A4: x1 in S1 ; :: thesis: x1 in S2
then reconsider x2 = x1 as Element of L ;
x2 is completely-irreducible by A2, A4;
hence x1 in S2 by A3; :: thesis: verum

end;

thus ( x1 in S2 implies x1 in S1 ) :: thesis: verum

proof

assume A5: x1 in S2 ; :: thesis: x1 in S1
then reconsider x2 = x1 as Element of L ;
x2 is completely-irreducible by A3, A5;
hence x1 in S1 by A2; :: thesis: verum

end;

end;

hence S1 = S2 by TARSKI:1; :: thesis: verum