the carrier of (RealPoset [.0 ,1.]) = [.0 ,1.] by Def3;
hence RealPoset [.0 ,1.] is interval by Def2; :: thesis: verum