:: deftheorem defines 01-dominant FUZIMPL1:def 6 :
for f being BinOp of [.0,1.] holds
( f is 01-dominant iff f . (0,1) = 1 );