let T be non empty TopSpace; :: thesis: for A, B being Subset of T
for G being Rain of A,B
for p being Point of T ex R being Subset of ExtREAL st
for x being set holds
( x in R iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) )
let A, B be Subset of T; :: thesis: for G being Rain of A,B
for p being Point of T ex R being Subset of ExtREAL st
for x being set holds
( x in R iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) )
let G be Rain of A,B; :: thesis: for p being Point of T ex R being Subset of ExtREAL st
for x being set holds
( x in R iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) )
let p be Point of T; :: thesis: ex R being Subset of ExtREAL st
for x being set holds
( x in R iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) )
defpred S₁[ set ] means for s being Real st s = $1 holds
not p in (Tempest G) . s;
ex X being set st
for x being set holds
( x in X iff ( x in DYADIC & S₁[x] ) ) from XBOOLE_0:sch 1();
then consider R being set such that
A1: for x being set holds
( x in R iff ( x in DYADIC & S₁[x] ) ) ;
R c= REAL

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in R or x in REAL )
assume x in R ; :: thesis: x in REAL
then x in DYADIC by A1;
hence x in REAL ; :: thesis: verum

end;

then reconsider R = R as Subset of ExtREAL by NUMBERS:31, XBOOLE_1:1;
take R ; :: thesis: for x being set holds
( x in R iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) )
thus for x being set holds
( x in R iff ( x in DYADIC & ( for s being Real st s = x holds
not p in (Tempest G) . s ) ) ) by A1; :: thesis: verum