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

assume a1: I is satisfying_(OP) ; :: thesis: ( I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(NC) & I is satisfying_(LB) & I is satisfying_(RB) & I is satisfying_(IP) )

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

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

T3: I is satisfying_(LB)

assume a1: I is satisfying_(OP) ; :: thesis: ( I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(NC) & I is satisfying_(LB) & I is satisfying_(RB) & I is satisfying_(IP) )

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

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

T3: I is satisfying_(LB)

proof

I is satisfying_(RB)
let y be Element of [.0,1.]; :: according to FUZIMPL1:def 26 :: thesis: I . (K38(),y) = 1

0 <= y by XXREAL_1:1;

hence I . (K38(),y) = 1 by a1, A2; :: thesis: verum

end;0 <= y by XXREAL_1:1;

hence I . (K38(),y) = 1 by a1, A2; :: thesis: verum

proof

hence
( I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(NC) & I is satisfying_(LB) & I is satisfying_(RB) & I is satisfying_(IP) )
by T3, a1; :: thesis: verum
let x be Element of [.0,1.]; :: according to FUZIMPL1:def 27 :: thesis: I . (x,1) = 1

x <= 1 by XXREAL_1:1;

hence I . (x,1) = 1 by a1, A3; :: thesis: verum

end;x <= 1 by XXREAL_1:1;

hence I . (x,1) = 1 by a1, A3; :: thesis: verum