let a, b be Real_Sequence; :: thesis: IntervalSequence (a,b) is SetSequence of (Euclid 1)
REAL 1 = the carrier of (TOP-REAL 1) by EUCLID:22
.= the carrier of (Euclid 1) by EUCLID:67 ;
hence IntervalSequence (a,b) is SetSequence of (Euclid 1) ; :: thesis: verum