let R be non empty RelStr ; :: thesis: ( R is interval implies R is bounded )
assume A1: R is real ; :: according to LFUZZY_0:def 2 :: thesis: ( for a, b being real number holds
( not a <= b or not the carrier of R = [.a,b.] ) or R is bounded )
given x, y being real number such that A2: ( x <= y & the carrier of R = [.x,y.] ) ; :: thesis: R is bounded
ex x being real number st
( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x >= y ) )

proof

take y ; :: thesis: ( y in the carrier of R & ( for y being real number st y in the carrier of R holds
y >= y ) )
thus y in the carrier of R by A2, XXREAL_1:1; :: thesis: for y being real number st y in the carrier of R holds
y >= y
let z be real number ; :: thesis: ( z in the carrier of R implies y >= z )
assume z in the carrier of R ; :: thesis: y >= z
hence y >= z by A2, XXREAL_1:1; :: thesis: verum

end;

then A3: R is upper-bounded by A1, Th7;
ex x being real number st
( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x <= y ) )

proof

take x ; :: thesis: ( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x <= y ) )
thus x in the carrier of R by A2, XXREAL_1:1; :: thesis: for y being real number st y in the carrier of R holds
x <= y
let z be real number ; :: thesis: ( z in the carrier of R implies x <= z )
assume z in the carrier of R ; :: thesis: x <= z
hence x <= z by A2, XXREAL_1:1; :: thesis: verum

end;

then R is lower-bounded by A1, Th6;
hence R is bounded by A3; :: thesis: verum