let A1, A2 be Subset of REAL; :: thesis: ( ( for x being R_eal holds
( x in A1 iff P1[x] ) ) & ( for x being R_eal holds
( x in A2 iff P1[x] ) ) implies A1 = A2 )
assume that
A1: for x being R_eal holds
( x in A1 iff P1[x] ) and
A2: for x being R_eal holds
( x in A2 iff P1[x] ) ; :: thesis: A1 = A2
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 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;
P1[x] by A1, A3;
hence x in A2 by A2; :: thesis: verum
end;
let x be Real; :: according to MEMBERED:def 9 :: thesis: ( not x in A2 or x in A1 )
assume A4: x in A2 ; :: thesis: x in A1
then x in REAL ;
then reconsider x = x as R_eal by NUMBERS:31;
P1[x] by A2, A4;
hence x in A1 by A1; :: thesis: verum