let X be BCI-algebra; :: thesis: 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
let Y be SubAlgebra of X; :: thesis: for x, y being Element of X
for x9, y9 being Element of Y st x = x9 & y = y9 holds
x \ y = x9 \ y9
let x, y be Element of X; :: thesis: for x9, y9 being Element of Y st x = x9 & y = y9 holds
x \ y = x9 \ y9
let x9, y9 be Element of Y; :: thesis: ( x = x9 & y = y9 implies x \ y = x9 \ y9 )
assume A1: ( x = x9 & y = y9 ) ; :: thesis: x \ y = x9 \ y9
A2: [x9,y9] in [: the carrier of Y, the carrier of Y:] by ZFMISC_1:87;
x9 \ y9 = ( the InternalDiff of X || the carrier of Y) . (x9,y9) by BCIALG_1:def 10
.= x \ y by A1, A2, FUNCT_1:49 ;
hence x \ y = x9 \ y9 ; :: thesis: verum