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

assume a1: I is satisfying_(NP) ; :: thesis: ( I is satisfying_(I4) & I is satisfying_(I5) )

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

hence I is satisfying_(I4) by a1; :: thesis: I is satisfying_(I5)

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

hence I is satisfying_(I5) by a1; :: thesis: verum

assume a1: I is satisfying_(NP) ; :: thesis: ( I is satisfying_(I4) & I is satisfying_(I5) )

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

hence I is satisfying_(I4) by a1; :: thesis: I is satisfying_(I5)

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

hence I is satisfying_(I5) by a1; :: thesis: verum