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 :: according to XBOOLE_0:def 10 :: thesis: Y c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Y )
assume A4: x in X ; :: thesis: x in Y
then reconsider x1 = x as Element of L ;
x1 is prime by A2, A4;
hence x in Y by A3; :: thesis: verum

end;

thus Y c= X :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in X )
assume A5: x in Y ; :: thesis: x in X
then reconsider x1 = x as Element of L ;
x1 is prime by A3, A5;
hence x in X by A2; :: thesis: verum

end;