theorem :: BCIALG_4:18

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