thus Imf X,X is symmetric :: thesis: ( Imf X,X is transitive & Imf X,X is reflexive & Imf X,X is antisymmetric )

proof

let x, y be Element of X; :: according to LFUZZY_1:def 5 :: thesis: (Imf X,X) . x,y = (Imf X,X) . y,x

per cases ( x = y or not x = y ) ;

suppose x = y ; :: thesis: (Imf X,X) . x,y = (Imf X,X) . y,x

hence (Imf X,X) . x,y = (Imf X,X) . y,x ; :: thesis: verum

end;

suppose A1: not x = y ; :: thesis: (Imf X,X) . x,y = (Imf X,X) . y,x

hence (Imf X,X) . x,y = 0 by FUZZY_4:25
.= (Imf X,X) . y,x by A1, FUZZY_4:25 ;
:: thesis: verum

end;

end;

end;

thus Imf X,X is transitive :: thesis: ( Imf X,X is reflexive & Imf X,X is antisymmetric )

proof

let x, y, z be Element of X; :: according to LFUZZY_1:def 7 :: thesis: ((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) <<= (Imf X,X) . [x,z]

per cases ( x = z or not x = z ) ;

suppose A2: x = z ; :: thesis: ((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) <<= (Imf X,X) . [x,z]

thus ((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) <<= (Imf X,X) . [x,z] :: thesis: verum

proof

per cases ( x = y or not x = y ) ;

suppose A3: x = y ; :: thesis: ((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) <<= (Imf X,X) . [x,z]

((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) = min ((Imf X,X) . x,y),((Imf X,X) . y,z)
.= 1 by A2, A3, FUZZY_4:25 ;
then ((Imf X,X) . x,y) "/\" ((Imf X,X) . y,z) <= (Imf X,X) . x,z by A2, FUZZY_4:25;
hence ((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) <<= (Imf X,X) . [x,z] by LFUZZY_0:3; :: thesis: verum

end;

suppose A4: not x = y ; :: thesis: ((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) <<= (Imf X,X) . [x,z]

((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) = min ((Imf X,X) . x,y),((Imf X,X) . y,z)
.= min ((Imf X,X) . x,y),0 by A2, A4, FUZZY_4:25
.= min 0 ,0 by A4, FUZZY_4:25
.= 0 ;
then ((Imf X,X) . x,y) "/\" ((Imf X,X) . y,z) <= (Imf X,X) . x,z by A2, FUZZY_4:25;
hence ((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) <<= (Imf X,X) . [x,z] by LFUZZY_0:3; :: thesis: verum

end;

end;

end;

end;

suppose A5: not x = z ; :: thesis: ((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) <<= (Imf X,X) . [x,z]

thus ((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) <<= (Imf X,X) . [x,z] :: thesis: verum

proof

per cases ( x = y or x <> y ) ;

suppose A6: x = y ; :: thesis: ((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) <<= (Imf X,X) . [x,z]

((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) = min ((Imf X,X) . x,y),((Imf X,X) . y,z)
.= min ((Imf X,X) . x,y),0 by A5, A6, FUZZY_4:25
.= min 1,0 by A6, FUZZY_4:25
.= 0 by XXREAL_0:def 9 ;
then ((Imf X,X) . x,y) "/\" ((Imf X,X) . y,z) <= (Imf X,X) . x,z by A5, FUZZY_4:25;
hence ((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) <<= (Imf X,X) . [x,z] by LFUZZY_0:3; :: thesis: verum

end;

suppose A7: x <> y ; :: thesis: ((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) <<= (Imf X,X) . [x,z]

thus ((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) <<= (Imf X,X) . [x,z] :: thesis: verum

proof

per cases ( y = z or y <> z ) ;

suppose A8: y = z ; :: thesis: ((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) <<= (Imf X,X) . [x,z]

((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) = min ((Imf X,X) . x,y),((Imf X,X) . y,z)
.= min ((Imf X,X) . x,y),1 by A8, FUZZY_4:25
.= min 0 ,1 by A7, FUZZY_4:25
.= 0 by XXREAL_0:def 9 ;
then ((Imf X,X) . x,y) "/\" ((Imf X,X) . y,z) <= (Imf X,X) . x,z by A5, FUZZY_4:25;
hence ((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) <<= (Imf X,X) . [x,z] by LFUZZY_0:3; :: thesis: verum

end;

suppose A9: y <> z ; :: thesis: ((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) <<= (Imf X,X) . [x,z]

((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) = min ((Imf X,X) . x,y),((Imf X,X) . y,z)
.= min ((Imf X,X) . x,y),0 by A9, FUZZY_4:25
.= min 0 ,0 by A7, FUZZY_4:25
.= 0 ;
then ((Imf X,X) . x,y) "/\" ((Imf X,X) . y,z) <= (Imf X,X) . x,z by A5, FUZZY_4:25;
hence ((Imf X,X) . [x,y]) "/\" ((Imf X,X) . [y,z]) <<= (Imf X,X) . [x,z] by LFUZZY_0:3; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

thus Imf X,X is reflexive :: thesis: Imf X,X is antisymmetric

proof

thus for x being Element of X holds (Imf X,X) . x,x = 1 by FUZZY_4:25; :: according to LFUZZY_1:def 3 :: thesis: verum

end;

thus for x, y being Element of X st (Imf X,X) . x,y <> 0 & (Imf X,X) . y,x <> 0 holds
x = y by FUZZY_4:25; :: according to LFUZZY_1:def 8 :: thesis: verum