theorem Th18: :: BCIALG_4:19

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