defpred S_{1}[ object ] means for s being Real st s = $1 holds

not p in (Tempest G) . s;

consider R being set such that

A1: for x being object holds

( x in R iff ( x in DYADIC & S_{1}[x] ) )
from XBOOLE_0:sch 1();

R c= REAL

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

not p in (Tempest G) . s;

consider R being set such that

A1: for x being object holds

( x in R iff ( x in DYADIC & S

R c= REAL

proof

then reconsider R = R as Subset of ExtREAL by NUMBERS:31, XBOOLE_1:1;
let x be object ; :: 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;assume x in R ; :: thesis: x in REAL

then x in DYADIC by A1;

hence x in REAL ; :: thesis: verum

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