:: deftheorem Def13 defines proper BCIALG_1:def 13 :
for X being BCI-algebra
for IT being SubAlgebra of X holds
( IT is proper iff IT <> X );