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
for x1 being object holds
( x1 in S1 iff x1 in S2 ) by A2, A3;
hence S1 = S2 by TARSKI:2; :: thesis: verum