:: deftheorem defines ./. BCIALG_2:def 19 :
for X being BCI-algebra
for E being Congruence of X holds X ./. E = BCIStr_0(# (Class E),(EqClaOp E),(zeroEqC E) #);