for X being BCI-Algebra_with_Condition(S) holds 0. X is_a_unity_wrt the ExternalDiff of X