let TD1, TD2 be Subset of (REAL *); :: thesis: ( ( for x being object holds
( x in TD1 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) ) ) ) ) & ( for x being object holds
( x in TD2 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) ) ) ) ) implies TD1 = TD2 )
assume that
A1: for x being object holds
( x in TD1 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) ) ) ) and
A2: for x being object holds
( x in TD2 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) ) ) ) ; :: thesis: TD1 = TD2
A3: TD1 c= TD2

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in TD1 or x in TD2 )
assume x in TD1 ; :: thesis: x in TD2
then 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;
hence x in TD2 by A2; :: thesis: verum

end;

TD2 c= TD1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in TD2 or x in TD1 )
assume x in TD2 ; :: thesis: x in TD1
then 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 A2;
hence x in TD1 by A1; :: thesis: verum

end;

hence TD1 = TD2 by A3; :: thesis: verum