set X = [.0,1.];
consider R being strict RelStr such that
A1: ( the carrier of R = [.0,1.] & R is real ) by Th1;
take R ; :: thesis: ( R is interval & R is strict )
thus ( R is interval & R is strict ) by A1; :: thesis: verum