for X being BCI-Algebra_with_Condition(S) holds the ExternalDiff of X is having_a_unity