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