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 holds
( not a <= b or not the carrier of R = [.a,b.] ) or R is bounded )

given x, y being Real such that A2: x <= y and
A3: the carrier of R = [.x,y.] ; :: thesis: R is bounded
ex x being Real st
( x in the carrier of R & ( for y being Real st y in the carrier of R holds
x <= y ) )
proof
take x ; :: thesis: ( x in the carrier of R & ( for y being Real st y in the carrier of R holds
x <= y ) )

thus x in the carrier of R by ; :: thesis: for y being Real st y in the carrier of R holds
x <= y

let z be Real; :: thesis: ( z in the carrier of R implies x <= z )
assume z in the carrier of R ; :: thesis: x <= z
hence x <= z by ; :: thesis: verum
end;
then A4: R is lower-bounded by ;
ex x being Real st
( x in the carrier of R & ( for y being Real st y in the carrier of R holds
x >= y ) )
proof
take y ; :: thesis: ( y in the carrier of R & ( for y being Real st y in the carrier of R holds
y >= y ) )

thus y in the carrier of R by ; :: thesis: for y being Real st y in the carrier of R holds
y >= y

let z be Real; :: thesis: ( z in the carrier of R implies y >= z )
assume z in the carrier of R ; :: thesis: y >= z
hence y >= z by ; :: thesis: verum
end;
then R is upper-bounded by ;
hence R is bounded by A4; :: thesis: verum