let R be RelStr ; :: thesis: ( R is interval implies ( R is real & not R is empty ) )
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 real & not R is empty ) )
given a, b being real number such that A2: ( a <= b & the carrier of R = [.a,b.] ) ; :: thesis: ( R is real & not R is empty )
thus R is real by A1; :: thesis: not R is empty
thus not the carrier of R is empty by A2, XXREAL_1:1; :: according to STRUCT_0:def 1 :: thesis: verum