let X be BCI-algebra; :: thesis: for a being Element of X
for x, b being Element of AtomSet X st x is Element of BranchV b holds
a \ x = a \ b
set P = AtomSet X;
let a be Element of X; :: thesis: for x, b being Element of AtomSet X st x is Element of BranchV b holds
a \ x = a \ b
let x, b be Element of AtomSet X; :: thesis: ( x is Element of BranchV b implies a \ x = a \ b )
set B = BranchV b;
assume A0: x is Element of BranchV b ; :: thesis: a \ x = a \ b
A1: x in BranchV b by A0;
x in { x1 where x1 is Element of X : x1 is atom } ;
then consider x1 being Element of X such that
B1: ( x = x1 & x1 is atom ) ;
consider x3 being Element of X such that
C1: ( x = x3 & b <= x3 ) by A1;
b \ x = 0. X by C1, BCIALG_1:def 11;
hence a \ x = a \ b by B1, BCIALG_1:def 14; :: thesis: verum