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 )

( 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

hence
R1 = R2
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in R1 iff x in R2 )

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;hereby :: thesis: ( x in R2 implies x in R1 )

assume
x in R2
; :: thesis: x in R1assume
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;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

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