let I be BinOp of [.0,1.]; :: thesis: ( I is satisfying_(IP) implies ( I is satisfying_(I3) & I is satisfying_(I4) ) )

assume a1: I is satisfying_(IP) ; :: thesis: ( I is satisfying_(I3) & I is satisfying_(I4) )

A2: 0 in [.0,1.] by XXREAL_1:1;

1 in [.0,1.] by XXREAL_1:1;

hence ( I is satisfying_(I3) & I is satisfying_(I4) ) by a1, A2; :: thesis: verum

assume a1: I is satisfying_(IP) ; :: thesis: ( I is satisfying_(I3) & I is satisfying_(I4) )

A2: 0 in [.0,1.] by XXREAL_1:1;

1 in [.0,1.] by XXREAL_1:1;

hence ( I is satisfying_(I3) & I is satisfying_(I4) ) by a1, A2; :: thesis: verum