:: Formal Introduction to Fuzzy Implications
::
:: Copyright (c) 2017-2019 Association of Mizar Users

theorem MaxMinIn01: :: FUZIMPL1:1
for a, b being Element of [.0,1.] holds max (b,(min ((1 - a),(1 - b)))) in [.0,1.]
proof end;

theorem LukaIn01: :: FUZIMPL1:2
for a, b being Element of [.0,1.] holds min (1,((1 - a) + b)) in [.0,1.]
proof end;

theorem ReichenbachIn01: :: FUZIMPL1:3
for a, b being Element of [.0,1.] holds (1 - a) + (a * b) in [.0,1.]
proof end;

theorem Max1In01: :: FUZIMPL1:4
for a, b being Element of [.0,1.] holds max ((1 - a),b) in [.0,1.]
proof end;

theorem PowerIn01: :: FUZIMPL1:5
for a, b being Element of [.0,1.] st ( a > 0 or b > 0 ) holds
b to_power a in [.0,1.]
proof end;

theorem QuoIn01: :: FUZIMPL1:6
for a, b being Element of [.0,1.] st a > b holds
b / a in [.0,1.]
proof end;

definition
let f be BinOp of [.0,1.];
attr f is decreasing_on_1st means :DefDecr: :: FUZIMPL1:def 1
for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds
f . (x1,y) >= f . (x2,y);
attr f is increasing_on_2nd means :DefIncr: :: FUZIMPL1:def 2
for x, y1, y2 being Element of [.0,1.] st y1 <= y2 holds
f . (x,y1) <= f . (x,y2);
attr f is 00-dominant means :Def00: :: FUZIMPL1:def 3
f . (0,0) = 1;
attr f is 11-dominant means :Def11: :: FUZIMPL1:def 4
f . (1,1) = 1;
attr f is 10-weak means :Def10: :: FUZIMPL1:def 5
f . (1,0) = 0 ;
attr f is 01-dominant means :: FUZIMPL1:def 6
f . (0,1) = 1;
end;

:: deftheorem DefDecr defines decreasing_on_1st FUZIMPL1:def 1 :
for f being BinOp of [.0,1.] holds
( f is decreasing_on_1st iff for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds
f . (x1,y) >= f . (x2,y) );

:: deftheorem DefIncr defines increasing_on_2nd FUZIMPL1:def 2 :
for f being BinOp of [.0,1.] holds
( f is increasing_on_2nd iff for x, y1, y2 being Element of [.0,1.] st y1 <= y2 holds
f . (x,y1) <= f . (x,y2) );

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

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

:: deftheorem Def10 defines 10-weak FUZIMPL1:def 5 :
for f being BinOp of [.0,1.] holds
( f is 10-weak iff f . (1,0) = 0 );

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

:: Classical Implication
definition
let f be BinOp of [.0,1.];
attr f is with_properties_of_fuzzy_implication means :: FUZIMPL1:def 7
( f is decreasing_on_1st & f is increasing_on_2nd & f is 00-dominant & f is 11-dominant & f is 10-weak );
attr f is with_properties_of_classical_implication means :: FUZIMPL1:def 8
( f is 00-dominant & f is 01-dominant & f is 11-dominant & f is 10-weak );
end;

:: deftheorem defines with_properties_of_fuzzy_implication FUZIMPL1:def 7 :
for f being BinOp of [.0,1.] holds
( f is with_properties_of_fuzzy_implication iff ( f is decreasing_on_1st & f is increasing_on_2nd & f is 00-dominant & f is 11-dominant & f is 10-weak ) );

:: deftheorem defines with_properties_of_classical_implication FUZIMPL1:def 8 :
for f being BinOp of [.0,1.] holds
( f is with_properties_of_classical_implication iff ( f is 00-dominant & f is 01-dominant & f is 11-dominant & f is 10-weak ) );

definition
func I_{-1} -> BinOp of [.0,1.] means :I1Def: :: FUZIMPL1:def 9
for x, y being Element of [.0,1.] holds it . (x,y) = max ((1 - x),(min (x,y)));
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds b1 . (x,y) = max ((1 - x),(min (x,y)))
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b1 . (x,y) = max ((1 - x),(min (x,y))) ) & ( for x, y being Element of [.0,1.] holds b2 . (x,y) = max ((1 - x),(min (x,y))) ) holds
b1 = b2
proof end;
end;

:: deftheorem I1Def defines I_{-1} FUZIMPL1:def 9 :
for b1 being BinOp of [.0,1.] holds
( b1 = I_{-1} iff for x, y being Element of [.0,1.] holds b1 . (x,y) = max ((1 - x),(min (x,y))) );

registration
coherence
proof end;
end;

definition
func I_{-2} -> BinOp of [.0,1.] means :I2Def: :: FUZIMPL1:def 10
for x, y being Element of [.0,1.] holds it . (x,y) = max (y,(min ((1 - x),(1 - y))));
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds b1 . (x,y) = max (y,(min ((1 - x),(1 - y))))
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b1 . (x,y) = max (y,(min ((1 - x),(1 - y)))) ) & ( for x, y being Element of [.0,1.] holds b2 . (x,y) = max (y,(min ((1 - x),(1 - y)))) ) holds
b1 = b2
proof end;
end;

:: deftheorem I2Def defines I_{-2} FUZIMPL1:def 10 :
for b1 being BinOp of [.0,1.] holds
( b1 = I_{-2} iff for x, y being Element of [.0,1.] holds b1 . (x,y) = max (y,(min ((1 - x),(1 - y)))) );

registration
coherence
proof end;
end;

definition
func I_{-3} -> BinOp of [.0,1.] means :I3Def: :: FUZIMPL1:def 11
for x, y being Element of [.0,1.] holds
( ( y < 1 implies it . (x,y) = 0 ) & ( y = 1 implies it . (x,y) = 1 ) );
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( y < 1 implies b1 . (x,y) = 0 ) & ( y = 1 implies b1 . (x,y) = 1 ) )
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( y < 1 implies b1 . (x,y) = 0 ) & ( y = 1 implies b1 . (x,y) = 1 ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( y < 1 implies b2 . (x,y) = 0 ) & ( y = 1 implies b2 . (x,y) = 1 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem I3Def defines I_{-3} FUZIMPL1:def 11 :
for b1 being BinOp of [.0,1.] holds
( b1 = I_{-3} iff for x, y being Element of [.0,1.] holds
( ( y < 1 implies b1 . (x,y) = 0 ) & ( y = 1 implies b1 . (x,y) = 1 ) ) );

registration
coherence
proof end;
end;

definition
func I_{-4} -> BinOp of [.0,1.] means :I4Def: :: FUZIMPL1:def 12
for x, y being Element of [.0,1.] holds
( ( x = 0 implies it . (x,y) = 1 ) & ( x > 0 implies it . (x,y) = 0 ) );
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x = 0 implies b1 . (x,y) = 1 ) & ( x > 0 implies b1 . (x,y) = 0 ) )
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x = 0 implies b1 . (x,y) = 1 ) & ( x > 0 implies b1 . (x,y) = 0 ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x = 0 implies b2 . (x,y) = 1 ) & ( x > 0 implies b2 . (x,y) = 0 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem I4Def defines I_{-4} FUZIMPL1:def 12 :
for b1 being BinOp of [.0,1.] holds
( b1 = I_{-4} iff for x, y being Element of [.0,1.] holds
( ( x = 0 implies b1 . (x,y) = 1 ) & ( x > 0 implies b1 . (x,y) = 0 ) ) );

registration
coherence
proof end;
end;

definition
func I_{-5} -> BinOp of [.0,1.] means :I5Def: :: FUZIMPL1:def 13
for x, y being Element of [.0,1.] holds it . (x,y) = 1;
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds b1 . (x,y) = 1
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b1 . (x,y) = 1 ) & ( for x, y being Element of [.0,1.] holds b2 . (x,y) = 1 ) holds
b1 = b2
proof end;
end;

:: deftheorem I5Def defines I_{-5} FUZIMPL1:def 13 :
for b1 being BinOp of [.0,1.] holds
( b1 = I_{-5} iff for x, y being Element of [.0,1.] holds b1 . (x,y) = 1 );

registration
coherence
proof end;
end;

definition
func Lukasiewicz_implication -> BinOp of [.0,1.] means :Luk: :: FUZIMPL1:def 14
for x, y being Element of [.0,1.] holds it . (x,y) = min (1,((1 - x) + y));
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds b1 . (x,y) = min (1,((1 - x) + y))
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b1 . (x,y) = min (1,((1 - x) + y)) ) & ( for x, y being Element of [.0,1.] holds b2 . (x,y) = min (1,((1 - x) + y)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Luk defines Lukasiewicz_implication FUZIMPL1:def 14 :
for b1 being BinOp of [.0,1.] holds
( b1 = Lukasiewicz_implication iff for x, y being Element of [.0,1.] holds b1 . (x,y) = min (1,((1 - x) + y)) );

registration
coherence
proof end;
end;

registration
cluster V1() V4([:[.0,1.],[.0,1.]:]) V5([.0,1.]) Function-like V29([:[.0,1.],[.0,1.]:],[.0,1.]) with_properties_of_fuzzy_implication for Element of bool [:[:[.0,1.],[.0,1.]:],[.0,1.]:];
existence
ex b1 being BinOp of [.0,1.] st b1 is with_properties_of_fuzzy_implication
proof end;
end;

registration
coherence
for b1 being BinOp of [.0,1.] st b1 is with_properties_of_fuzzy_implication holds
( b1 is decreasing_on_1st & b1 is increasing_on_2nd & b1 is 00-dominant & b1 is 11-dominant & b1 is 10-weak )
;
coherence
for b1 being BinOp of [.0,1.] st b1 is decreasing_on_1st & b1 is increasing_on_2nd & b1 is 00-dominant & b1 is 01-dominant & b1 is 11-dominant & b1 is 10-weak holds
b1 is with_properties_of_fuzzy_implication
;
coherence
for b1 being BinOp of [.0,1.] st b1 is with_properties_of_classical_implication holds
( b1 is 00-dominant & b1 is 01-dominant & b1 is 11-dominant & b1 is 10-weak )
;
coherence
for b1 being BinOp of [.0,1.] st b1 is 00-dominant & b1 is 01-dominant & b1 is 11-dominant & b1 is 10-weak holds
b1 is with_properties_of_classical_implication
;
coherence
for b1 being BinOp of [.0,1.] st b1 is with_properties_of_fuzzy_implication holds
b1 is with_properties_of_classical_implication
proof end;
end;

definition end;

definition
func FI -> set equals :: FUZIMPL1:def 15
{ f where f is Fuzzy_Implication : verum } ;
coherence
{ f where f is Fuzzy_Implication : verum } is set
;
end;

:: deftheorem defines FI FUZIMPL1:def 15 :
FI = { f where f is Fuzzy_Implication : verum } ;

definition
func Goedel_implication -> BinOp of [.0,1.] means :Goedel: :: FUZIMPL1:def 16
for x, y being Element of [.0,1.] holds
( ( x <= y implies it . (x,y) = 1 ) & ( x > y implies it . (x,y) = y ) );
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = y ) )
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = y ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b2 . (x,y) = 1 ) & ( x > y implies b2 . (x,y) = y ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Goedel defines Goedel_implication FUZIMPL1:def 16 :
for b1 being BinOp of [.0,1.] holds
( b1 = Goedel_implication iff for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = y ) ) );

registration
coherence
proof end;
end;

definition
func Reichenbach_implication -> BinOp of [.0,1.] means :Reichen: :: FUZIMPL1:def 17
for x, y being Element of [.0,1.] holds it . (x,y) = (1 - x) + (x * y);
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds b1 . (x,y) = (1 - x) + (x * y)
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b1 . (x,y) = (1 - x) + (x * y) ) & ( for x, y being Element of [.0,1.] holds b2 . (x,y) = (1 - x) + (x * y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Reichen defines Reichenbach_implication FUZIMPL1:def 17 :
for b1 being BinOp of [.0,1.] holds
( b1 = Reichenbach_implication iff for x, y being Element of [.0,1.] holds b1 . (x,y) = (1 - x) + (x * y) );

registration
coherence
proof end;
end;

definition
func Kleene-Dienes_implication -> BinOp of [.0,1.] means :Kleene: :: FUZIMPL1:def 18
for x, y being Element of [.0,1.] holds it . (x,y) = max ((1 - x),y);
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds b1 . (x,y) = max ((1 - x),y)
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds b1 . (x,y) = max ((1 - x),y) ) & ( for x, y being Element of [.0,1.] holds b2 . (x,y) = max ((1 - x),y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Kleene defines Kleene-Dienes_implication FUZIMPL1:def 18 :
for b1 being BinOp of [.0,1.] holds
( b1 = Kleene-Dienes_implication iff for x, y being Element of [.0,1.] holds b1 . (x,y) = max ((1 - x),y) );

registration
coherence
proof end;
end;

definition
func Goguen_implication -> BinOp of [.0,1.] means :Goguen: :: FUZIMPL1:def 19
for x, y being Element of [.0,1.] holds
( ( x <= y implies it . (x,y) = 1 ) & ( x > y implies it . (x,y) = y / x ) );
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = y / x ) )
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = y / x ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b2 . (x,y) = 1 ) & ( x > y implies b2 . (x,y) = y / x ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Goguen defines Goguen_implication FUZIMPL1:def 19 :
for b1 being BinOp of [.0,1.] holds
( b1 = Goguen_implication iff for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = y / x ) ) );

registration
coherence
proof end;
end;

definition
func Rescher_implication -> BinOp of [.0,1.] means :Rescher: :: FUZIMPL1:def 20
for x, y being Element of [.0,1.] holds
( ( x <= y implies it . (x,y) = 1 ) & ( x > y implies it . (x,y) = 0 ) );
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = 0 ) )
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = 0 ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b2 . (x,y) = 1 ) & ( x > y implies b2 . (x,y) = 0 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Rescher defines Rescher_implication FUZIMPL1:def 20 :
for b1 being BinOp of [.0,1.] holds
( b1 = Rescher_implication iff for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = 0 ) ) );

registration
coherence
proof end;
end;

definition
func Yager_implication -> BinOp of [.0,1.] means :Yager: :: FUZIMPL1:def 21
for x, y being Element of [.0,1.] holds
( ( x = y & y = 0 implies it . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies it . (x,y) = y to_power x ) );
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x = y & y = 0 implies b1 . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies b1 . (x,y) = y to_power x ) )
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x = y & y = 0 implies b1 . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies b1 . (x,y) = y to_power x ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x = y & y = 0 implies b2 . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies b2 . (x,y) = y to_power x ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Yager defines Yager_implication FUZIMPL1:def 21 :
for b1 being BinOp of [.0,1.] holds
( b1 = Yager_implication iff for x, y being Element of [.0,1.] holds
( ( x = y & y = 0 implies b1 . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies b1 . (x,y) = y to_power x ) ) );

registration
coherence
proof end;
end;

definition
func Weber_implication -> BinOp of [.0,1.] means :Weber: :: FUZIMPL1:def 22
for x, y being Element of [.0,1.] holds
( ( x < 1 implies it . (x,y) = 1 ) & ( x = 1 implies it . (x,y) = y ) );
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x < 1 implies b1 . (x,y) = 1 ) & ( x = 1 implies b1 . (x,y) = y ) )
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x < 1 implies b1 . (x,y) = 1 ) & ( x = 1 implies b1 . (x,y) = y ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x < 1 implies b2 . (x,y) = 1 ) & ( x = 1 implies b2 . (x,y) = y ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Weber defines Weber_implication FUZIMPL1:def 22 :
for b1 being BinOp of [.0,1.] holds
( b1 = Weber_implication iff for x, y being Element of [.0,1.] holds
( ( x < 1 implies b1 . (x,y) = 1 ) & ( x = 1 implies b1 . (x,y) = y ) ) );

registration
coherence
proof end;
end;

definition
func Fodor_implication -> BinOp of [.0,1.] means :Fodor: :: FUZIMPL1:def 23
for x, y being Element of [.0,1.] holds
( ( x <= y implies it . (x,y) = 1 ) & ( x > y implies it . (x,y) = max ((1 - x),y) ) );
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = max ((1 - x),y) ) )
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = max ((1 - x),y) ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( x <= y implies b2 . (x,y) = 1 ) & ( x > y implies b2 . (x,y) = max ((1 - x),y) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Fodor defines Fodor_implication FUZIMPL1:def 23 :
for b1 being BinOp of [.0,1.] holds
( b1 = Fodor_implication iff for x, y being Element of [.0,1.] holds
( ( x <= y implies b1 . (x,y) = 1 ) & ( x > y implies b1 . (x,y) = max ((1 - x),y) ) ) );

registration
coherence
proof end;
end;

definition
func I_{0} -> BinOp of [.0,1.] means :I0Impl: :: FUZIMPL1:def 24
for x, y being Element of [.0,1.] holds
( ( ( x = 0 or y = 1 ) implies it . (x,y) = 1 ) & ( x > 0 & y < 1 implies it . (x,y) = 0 ) );
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( ( x = 0 or y = 1 ) implies b1 . (x,y) = 1 ) & ( x > 0 & y < 1 implies b1 . (x,y) = 0 ) )
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( ( x = 0 or y = 1 ) implies b1 . (x,y) = 1 ) & ( x > 0 & y < 1 implies b1 . (x,y) = 0 ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( ( x = 0 or y = 1 ) implies b2 . (x,y) = 1 ) & ( x > 0 & y < 1 implies b2 . (x,y) = 0 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem I0Impl defines I_{0} FUZIMPL1:def 24 :
for b1 being BinOp of [.0,1.] holds
( b1 = I_{0} iff for x, y being Element of [.0,1.] holds
( ( ( x = 0 or y = 1 ) implies b1 . (x,y) = 1 ) & ( x > 0 & y < 1 implies b1 . (x,y) = 0 ) ) );

registration
coherence
proof end;
end;

definition
func I_{1} -> BinOp of [.0,1.] means :I1Impl: :: FUZIMPL1:def 25
for x, y being Element of [.0,1.] holds
( ( ( x < 1 or y > 0 ) implies it . (x,y) = 1 ) & ( x = 1 & y = 0 implies it . (x,y) = 0 ) );
existence
ex b1 being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( ( x < 1 or y > 0 ) implies b1 . (x,y) = 1 ) & ( x = 1 & y = 0 implies b1 . (x,y) = 0 ) )
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x, y being Element of [.0,1.] holds
( ( ( x < 1 or y > 0 ) implies b1 . (x,y) = 1 ) & ( x = 1 & y = 0 implies b1 . (x,y) = 0 ) ) ) & ( for x, y being Element of [.0,1.] holds
( ( ( x < 1 or y > 0 ) implies b2 . (x,y) = 1 ) & ( x = 1 & y = 0 implies b2 . (x,y) = 0 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem I1Impl defines I_{1} FUZIMPL1:def 25 :
for b1 being BinOp of [.0,1.] holds
( b1 = I_{1} iff for x, y being Element of [.0,1.] holds
( ( ( x < 1 or y > 0 ) implies b1 . (x,y) = 1 ) & ( x = 1 & y = 0 implies b1 . (x,y) = 0 ) ) );

registration
coherence
proof end;
end;

definition
let f be BinOp of [.0,1.];
attr f is satisfying_(LB) means :: FUZIMPL1:def 26
for y being Element of [.0,1.] holds f . (0,y) = 1;
attr f is satisfying_(RB) means :: FUZIMPL1:def 27
for x being Element of [.0,1.] holds f . (x,1) = 1;
end;

:: deftheorem defines satisfying_(LB) FUZIMPL1:def 26 :
for f being BinOp of [.0,1.] holds
( f is satisfying_(LB) iff for y being Element of [.0,1.] holds f . (0,y) = 1 );

:: deftheorem defines satisfying_(RB) FUZIMPL1:def 27 :
for f being BinOp of [.0,1.] holds
( f is satisfying_(RB) iff for x being Element of [.0,1.] holds f . (x,1) = 1 );

theorem LBProp: :: FUZIMPL1:7
for fi being Fuzzy_Implication
for y being Element of [.0,1.] holds fi . (0,y) = 1
proof end;

theorem RBProp: :: FUZIMPL1:8
for fi being Fuzzy_Implication
for x being Element of [.0,1.] holds fi . (x,1) = 1
proof end;

registration
coherence
for b1 being Fuzzy_Implication holds
( b1 is satisfying_(LB) & b1 is satisfying_(RB) )
by ;
end;

theorem :: FUZIMPL1:9
for fi being Fuzzy_Implication holds I_{0} <= fi
proof end;

theorem :: FUZIMPL1:10
for fi being Fuzzy_Implication holds fi <= I_{1}
proof end;