:: deftheorem Def10 defines SubAlgebra BCIALG_1:def 10 :
for X, b₂ being BCI-algebra holds
( b₂ is SubAlgebra of X iff ( 0. b₂ = 0. X & the carrier of b₂ c= the carrier of X & the InternalDiff of b₂ = the InternalDiff of X || the carrier of b₂ ) );