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

now

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 Th7
.= the ExternalDiff of X . (b,a) ; :: thesis: verum

end;

hence the ExternalDiff of X is commutative by BINOP_1:def 2; :: thesis: verum