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)

let 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;

hence the ExternalDiff of X is commutative ; :: thesis: verum