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 ) )

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 ) )

hence R is bounded by A4; :: thesis: verum

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

then A4:
R is lower-bounded
by A1, Th6;
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 A2, A3, XXREAL_1:1; :: 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 A3, XXREAL_1:1; :: thesis: verum

end;x <= y ) )

thus x in the carrier of R by A2, A3, XXREAL_1:1; :: 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 A3, XXREAL_1:1; :: thesis: verum

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

then
R is upper-bounded
by A1, Th7;
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 A2, A3, XXREAL_1:1; :: 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 A3, XXREAL_1:1; :: thesis: verum

end;y >= y ) )

thus y in the carrier of R by A2, A3, XXREAL_1:1; :: 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 A3, XXREAL_1:1; :: thesis: verum

hence R is bounded by A4; :: thesis: verum