reconsider f = id [.0,1.] as UnOp of [.0,1.] ;
take f ; :: thesis: ( f is bijective & f is increasing )
thus f is bijective ; :: thesis: f is increasing
thus f is increasing ; :: thesis: verum