let R1, R2 be Subset of ExtREAL; :: thesis: ( ( for x being set holds
( x in R1 iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) ) ) & ( for x being set holds
( x in R2 iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) ) ) implies R1 = R2 )
assume that
A2: for x being set holds
( x in R1 iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) ) and
A3: for x being set holds
( x in R2 iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) ) ; :: thesis: R1 = R2
for x being object holds
( x in R1 iff x in R2 )
proof
let x be object ; :: thesis: ( x in R1 iff x in R2 )
hereby :: thesis: ( x in R2 implies x in R1 )
assume x in R1 ; :: thesis: x in R2
then ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) by A2;
hence x in R2 by A3; :: thesis: verum
end;
assume x in R2 ; :: thesis: x in R1
then ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) by A3;
hence x in R1 by A2; :: thesis: verum
end;
hence R1 = R2 by TARSKI:2; :: thesis: verum