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, Def2; :: thesis: verum