let R1, R2 be Subset of ; :: 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 R) . 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 R) . s ) ) ) ) implies R1 = R2 )
assume that
A1: for x being set holds
( x in R1 iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest R) . s ) ) ) and
A2: for x being set holds
( x in R2 iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest R) . s ) ) ) ; :: thesis: R1 = R2
for x being set holds
( x in R1 iff x in R2 )

proof

let x be set ; :: 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 R) . s ) ) by A1;
hence x in R2 by A2; :: 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 R) . s ) ) by A2;
hence x in R1 by A1; :: thesis: verum

end;

hence R1 = R2 by TARSKI:2; :: thesis: verum