let C be non empty set ; :: thesis: for f, g being Membership_Func of C st g c= holds
1_minus f c=
let f, g be Membership_Func of C; :: thesis: ( g c= implies 1_minus f c= )
assume A1: g c= ; :: thesis: 1_minus f c=
let x be Element of C; :: according to FUZZY_1:def 2 :: thesis: (1_minus g) . x <= (1_minus f) . x
f . x <= g . x by A1;
then 1 - (g . x) <= 1 - (f . x) by XREAL_1:10;
then (1_minus g) . x <= 1 - (f . x) by Def5;
hence (1_minus g) . x <= (1_minus f) . x by Def5; :: thesis: verum