theorem Th16: :: BCIALG_4:17

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