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

( 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