let X be BCI-Algebra_with_Condition(S); :: thesis: the ExternalDiff of X is commutative

now :: thesis: for a, b being Element of X holds the ExternalDiff of X . (a,b) = the ExternalDiff of X . (b,a)

hence
the ExternalDiff of X is commutative
; :: thesis: verumlet a, b be Element of X; :: thesis: the ExternalDiff of X . (a,b) = the ExternalDiff of X . (b,a)

thus the ExternalDiff of X . (a,b) = a * b

.= b * a by Th6

.= the ExternalDiff of X . (b,a) ; :: thesis: verum

end;thus the ExternalDiff of X . (a,b) = a * b

.= b * a by Th6

.= the ExternalDiff of X . (b,a) ; :: thesis: verum