let A1, A2 be Subset of REAL; :: thesis: ( ( for x being R_eal holds

( x in A1 iff P_{1}[x] ) ) & ( for x being R_eal holds

( x in A2 iff P_{1}[x] ) ) implies A1 = A2 )

assume that

A1: for x being R_eal holds

( x in A1 iff P_{1}[x] )
and

A2: for x being R_eal holds

( x in A2 iff P_{1}[x] )
; :: thesis: A1 = A2

thus A1 c= A2 :: according to XBOOLE_0:def 10 :: thesis: A2 c= A1

assume A4: x in A2 ; :: thesis: x in A1

then x in REAL ;

then reconsider x = x as R_eal by NUMBERS:31;

P_{1}[x]
by A2, A4;

hence x in A1 by A1; :: thesis: verum

( x in A1 iff P

( x in A2 iff P

assume that

A1: for x being R_eal holds

( x in A1 iff P

A2: for x being R_eal holds

( x in A2 iff P

thus A1 c= A2 :: according to XBOOLE_0:def 10 :: thesis: A2 c= A1

proof

let x be Real; :: according to MEMBERED:def 9 :: thesis: ( not x in A2 or x in A1 )
let x be Real; :: according to MEMBERED:def 9 :: thesis: ( not x in A1 or x in A2 )

assume A3: x in A1 ; :: thesis: x in A2

then x in REAL ;

then reconsider x = x as R_eal by NUMBERS:31;

P_{1}[x]
by A1, A3;

hence x in A2 by A2; :: thesis: verum

end;assume A3: x in A1 ; :: thesis: x in A2

then x in REAL ;

then reconsider x = x as R_eal by NUMBERS:31;

P

hence x in A2 by A2; :: thesis: verum

assume A4: x in A2 ; :: thesis: x in A1

then x in REAL ;

then reconsider x = x as R_eal by NUMBERS:31;

P

hence x in A1 by A1; :: thesis: verum