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

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

proof

thus
Imf (X,X) is transitive
:: thesis: ( Imf (X,X) is reflexive & Imf (X,X) is antisymmetric )
let x, y be Element of X; :: according to LFUZZY_1:def 5 :: thesis: (Imf (X,X)) . (x,y) = (Imf (X,X)) . (y,x)

end;proof

thus
Imf (X,X) is reflexive
; :: thesis: Imf (X,X) is antisymmetric
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]

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

end;

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

end;proof
end;

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

end;

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;.= 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

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;.= 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

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

end;proof
end;

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

end;

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;.= 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

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

end;proof
end;

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

end;

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;.= 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

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;.= 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

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