let X, Y be Subset of L; :: thesis: ( ( for x being Element of L holds
( x in X iff x is prime ) ) & ( for x being Element of L holds
( x in Y iff x is prime ) ) implies X = Y )
assume that
A2: for x being Element of L holds
( x in X iff x is prime ) and
A3: for x being Element of L holds
( x in Y iff x is prime ) ; :: thesis: X = Y
thus X c= Y by A2, A3; :: according to XBOOLE_0:def 10 :: thesis: Y c= X
thus Y c= X by A3, A2; :: thesis: verum