let X be BCI-algebra; :: thesis: for x, a, b being Element of AtomSet X st x is Element of BranchV b holds
a \ x = a \ b
set P = AtomSet X;
let x, a, b be Element of AtomSet X; :: thesis: ( x is Element of BranchV b implies a \ x = a \ b )
set B = BranchV b;
assume x is Element of BranchV b ; :: thesis: a \ x = a \ b
then x in BranchV b ;
then ex x3 being Element of X st
( x = x3 & b <= x3 ) ;
then A1: b \ x = 0. X ;
x in { x1 where x1 is Element of X : x1 is minimal } ;
then ex x1 being Element of X st
( x = x1 & x1 is minimal ) ;
hence a \ x = a \ b by A1; :: thesis: verum