let C be non empty set ; :: thesis: for F being FuzzySet of C st F is normalized holds
height F = 1
let F be FuzzySet of C; :: thesis: ( F is normalized implies height F = 1 )
assume F is normalized ; :: thesis: height F = 1
then consider x being Element of C such that
A1: F . x = 1 ;
x in C ;
then x in dom F by FUNCT_2:def 1;
then A2: 1 <= height F by XXREAL_2:4, FUNCT_1:3, A1;
height F <= 1 by HgtBnd;
hence height F = 1 by A2, XXREAL_0:1; :: thesis: verum