let r be real number ; :: thesis: ( r in the carrier of I(01) iff ( 0 < r & r < 1 ) )

hereby :: thesis: ( 0 < r & r < 1 implies r in the carrier of I(01) )

assume r in the carrier of I(01) ; :: thesis: ( 0 < r & r < 1 )
then r in ].0 ,1.[ by Def1;
hence ( 0 < r & r < 1 ) by XXREAL_1:4; :: thesis: verum

end;

assume ( 0 < r & r < 1 ) ; :: thesis: r in the carrier of I(01)
then r in ].0 ,1.[ by XXREAL_1:4;
hence r in the carrier of I(01) by Def1; :: thesis: verum