let X be BCI-algebra; :: thesis: for Y being SubAlgebra of X
for x, y being Element of X
for x', y' being Element of Y st x = x' & y = y' holds
x \ y = x' \ y'
let Y be SubAlgebra of X; :: thesis: for x, y being Element of X
for x', y' being Element of Y st x = x' & y = y' holds
x \ y = x' \ y'
let x, y be Element of X; :: thesis: for x', y' being Element of Y st x = x' & y = y' holds
x \ y = x' \ y'
let x', y' be Element of Y; :: thesis: ( x = x' & y = y' implies x \ y = x' \ y' )
assume A1: ( x = x' & y = y' ) ; :: thesis: x \ y = x' \ y'
A2: [x',y'] in [:the carrier of Y,the carrier of Y:] by ZFMISC_1:106;
x' \ y' = (the InternalDiff of X || the carrier of Y) . x',y' by BCIALG_1:def 10
.= x \ y by A1, A2, FUNCT_1:72 ;
hence x \ y = x' \ y' ; :: thesis: verum