defpred S₁[ object ] means ex s being non empty non-decreasing FinSequence of REAL st
( $1 = s & dom s = dom D & ( for i being Nat st i in dom s holds
s . i in divset (D,i) ) );
consider S being set such that
A1: for x being object holds
( x in S iff ( x in REAL * & S₁[x] ) ) from XBOOLE_0:sch 1();
take S ; :: thesis: ( S is Subset of (REAL *) & ( for x being object holds
( x in S iff ex s being non empty non-decreasing FinSequence of REAL st
( x = s & dom s = dom D & ( for i being Nat st i in dom s holds
s . i in divset (D,i) ) ) ) ) )
S c= REAL * by A1;
hence S is Subset of (REAL *) ; :: thesis: for x being object holds
( x in S iff ex s being non empty non-decreasing FinSequence of REAL st
( x = s & dom s = dom D & ( for i being Nat st i in dom s holds
s . i in divset (D,i) ) ) )
let x be object ; :: thesis: ( x in S iff ex s being non empty non-decreasing FinSequence of REAL st
( x = s & dom s = dom D & ( for i being Nat st i in dom s holds
s . i in divset (D,i) ) ) )
thus ( x in S implies ex s being non empty non-decreasing FinSequence of REAL st
( x = s & dom s = dom D & ( for i being Nat st i in dom s holds
s . i in divset (D,i) ) ) ) by A1; :: thesis: ( ex s being non empty non-decreasing FinSequence of REAL st
( x = s & dom s = dom D & ( for i being Nat st i in dom s holds
s . i in divset (D,i) ) ) implies x in S )
given s being non empty non-decreasing FinSequence of REAL such that A2: x = s and
A3: dom s = dom D and
A4: for i being Nat st i in dom s holds
s . i in divset (D,i) ; :: thesis: x in S
x in REAL * by A2, FINSEQ_1:def 11;
hence x in S by A2, A3, A4, A1; :: thesis: verum