take A = [.0,1.]; :: thesis: ( not A is trivial & A is closed_interval & A is closed )
( 0 in A & 1 in A ) ;
hence ( not A is trivial & A is closed_interval & A is closed ) by MEASURE5:def 3, ZFMISC_1:def 10; :: thesis: verum