let I be BinOp of [.0,1.]; :: thesis: ( I is satisfying_(LB) implies ( I is satisfying_(I3) & I is satisfying_(NC) ) )
assume a1: I is satisfying_(LB) ; :: thesis: ( I is satisfying_(I3) & I is satisfying_(NC) )
0 in [.0,1.] by XXREAL_1:1;
hence I is satisfying_(I3) by a1; :: thesis: I is satisfying_(NC)
1 in [.0,1.] by XXREAL_1:1;
hence I is satisfying_(NC) by a1; :: thesis: verum