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 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;
then A4: R is lower-bounded by A1, Th6;
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 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;
then R is upper-bounded by A1, Th7;
hence R is bounded by A4; :: thesis: verum