let r be Real; :: 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 that
A1: 0 < r and
A2: r < 1 ; :: thesis: r in the carrier of I(01)
r in ].0,1.[ by A1, A2, XXREAL_1:4;
hence r in the carrier of I(01) by Def1; :: thesis: verum