begin
Lm1:
for C being non empty set
for f, g being Membership_Func of C st g c= & f c= holds
f = g
begin
definition
let C be non
empty set ;
let h,
g be
Membership_Func of
C;
existence
ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = min ((h . c),(g . c))
uniqueness
for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = min ((h . c),(g . c)) ) & ( for c being Element of C holds b2 . c = min ((h . c),(g . c)) ) holds
b1 = b2
idempotence
for h being Membership_Func of C
for c being Element of C holds h . c = min ((h . c),(h . c))
;
commutativity
for b1, h, g being Membership_Func of C st ( for c being Element of C holds b1 . c = min ((h . c),(g . c)) ) holds
for c being Element of C holds b1 . c = min ((g . c),(h . c))
;
end;
definition
let C be non
empty set ;
let h,
g be
Membership_Func of
C;
existence
ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = max ((h . c),(g . c))
uniqueness
for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = max ((h . c),(g . c)) ) & ( for c being Element of C holds b2 . c = max ((h . c),(g . c)) ) holds
b1 = b2
idempotence
for h being Membership_Func of C
for c being Element of C holds h . c = max ((h . c),(h . c))
;
commutativity
for b1, h, g being Membership_Func of C st ( for c being Element of C holds b1 . c = max ((h . c),(g . c)) ) holds
for c being Element of C holds b1 . c = max ((g . c),(h . c))
;
end;
theorem
for
C being non
empty set for
h,
f,
g being
Membership_Func of
C holds
(
max (
h,
h)
= h &
min (
h,
h)
= h &
max (
h,
h)
= min (
h,
h) &
min (
f,
g)
= min (
g,
f) &
max (
f,
g)
= max (
g,
f) ) ;
theorem Th7:
for
C being non
empty set for
f,
g,
h being
Membership_Func of
C holds
(
max (
(max (f,g)),
h)
= max (
f,
(max (g,h))) &
min (
(min (f,g)),
h)
= min (
f,
(min (g,h))) )
theorem Th9:
for
C being non
empty set for
f,
g,
h being
Membership_Func of
C holds
(
min (
f,
(max (g,h)))
= max (
(min (f,g)),
(min (f,h))) &
max (
f,
(min (g,h)))
= min (
(max (f,g)),
(max (f,h))) )
begin
Lm2:
for C being non empty set
for f, g being Membership_Func of C st g c= holds
1_minus f c=
definition
let C be non
empty set ;
let h,
g be
Membership_Func of
C;
coherence
max ((min (h,(1_minus g))),(min ((1_minus h),g))) is Membership_Func of C
;
commutativity
for b1, h, g being Membership_Func of C st b1 = max ((min (h,(1_minus g))),(min ((1_minus h),g))) holds
b1 = max ((min (g,(1_minus h))),(min ((1_minus g),h)))
;
end;
theorem
for
C being non
empty set for
f,
g,
h being
Membership_Func of
C holds
min (
(min ((max (f,g)),(max (g,h)))),
(max (h,f)))
= max (
(max ((min (f,g)),(min (g,h)))),
(min (h,f)))