let C be non empty set ; :: thesis: for F being FuzzySet of C holds
( 0 <= height F & height F <= 1 )
let F be FuzzySet of C; :: thesis: ( 0 <= height F & height F <= 1 )
B0: 0 is LowerBound of rng F
proof
let x be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not x in rng F or 0 <= x )
assume x in rng F ; :: thesis: 0 <= x
then consider xx being object such that
B1: ( xx in dom F & x = F . xx ) by FUNCT_1:def 3;
reconsider xx = xx as Element of C by B1;
thus 0 <= x by B1, FUZZY_2:1; :: thesis: verum
end;
b2: 1 is UpperBound of rng F
proof
let x be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not x in rng F or x <= 1 )
assume x in rng F ; :: thesis: x <= 1
then consider xx being object such that
B1: ( xx in dom F & x = F . xx ) by FUNCT_1:def 3;
reconsider xx = xx as Element of C by B1;
thus x <= 1 by B1, FUZZY_2:1; :: thesis: verum
end;
inf (rng F) <= sup (rng F) by XXREAL_2:40;
hence ( 0 <= height F & height F <= 1 ) by b2, B0, XXREAL_2:def 4, XXREAL_2:def 3; :: thesis: verum