let A1, A2 be Subset of L; :: thesis: ( ( for x being Element of L holds
( x in A1 iff x is atom ) ) & ( for x being Element of L holds
( x in A2 iff x is atom ) ) implies A1 = A2 )
assume that
A2: for x being Element of L holds
( x in A1 iff x is atom ) and
A3: for x being Element of L holds
( x in A2 iff x is atom ) ; :: thesis: A1 = A2

now

let x be set ; :: thesis: ( ( x in A1 implies x in A2 ) & ( x in A2 implies x in A1 ) )
thus ( x in A1 implies x in A2 ) :: thesis: ( x in A2 implies x in A1 )

proof

assume A4: x in A1 ; :: thesis: x in A2
then reconsider x9 = x as Element of L ;
x9 is atom by A2, A4;
hence x in A2 by A3; :: thesis: verum

end;

thus ( x in A2 implies x in A1 ) :: thesis: verum

proof

assume A5: x in A2 ; :: thesis: x in A1
then reconsider x9 = x as Element of L ;
x9 is atom by A3, A5;
hence x in A1 by A2; :: thesis: verum

end;

end;

hence A1 = A2 by TARSKI:1; :: thesis: verum