theorem Th34: :: BCIALG_6:34

for X being BCI-algebra
for Y being SubAlgebra of X
for x, y being Element of X
for x9, y9 being Element of Y st x = x9 & y = y9 holds
x \ y = x9 \ y9