let X be BCI-algebra; :: thesis: for a, b being Element of AtomSet X st a <> b holds

(BranchV a) /\ (BranchV b) = {}

let a, b be Element of AtomSet X; :: thesis: ( a <> b implies (BranchV a) /\ (BranchV b) = {} )

assume A1: a <> b ; :: thesis: (BranchV a) /\ (BranchV b) = {}

assume (BranchV a) /\ (BranchV b) <> {} ; :: thesis: contradiction

then consider c being object such that

A2: c in (BranchV a) /\ (BranchV b) by XBOOLE_0:def 1;

reconsider z2 = c as Element of BranchV b by A2, XBOOLE_0:def 4;

reconsider z1 = c as Element of BranchV a by A2, XBOOLE_0:def 4;

z1 \ z2 in BranchV (a \ b) by Th39;

then 0. X in { x3 where x3 is Element of X : a \ b <= x3 } by Def5;

then ex x3 being Element of X st

( 0. X = x3 & a \ b <= x3 ) ;

then (a \ b) \ (0. X) = 0. X ;

then A3: a \ b = 0. X by Th2;

b in { xx where xx is Element of X : xx is atom } ;

then ex xx being Element of X st

( b = xx & xx is atom ) ;

hence contradiction by A1, A3; :: thesis: verum

(BranchV a) /\ (BranchV b) = {}

let a, b be Element of AtomSet X; :: thesis: ( a <> b implies (BranchV a) /\ (BranchV b) = {} )

assume A1: a <> b ; :: thesis: (BranchV a) /\ (BranchV b) = {}

assume (BranchV a) /\ (BranchV b) <> {} ; :: thesis: contradiction

then consider c being object such that

A2: c in (BranchV a) /\ (BranchV b) by XBOOLE_0:def 1;

reconsider z2 = c as Element of BranchV b by A2, XBOOLE_0:def 4;

reconsider z1 = c as Element of BranchV a by A2, XBOOLE_0:def 4;

z1 \ z2 in BranchV (a \ b) by Th39;

then 0. X in { x3 where x3 is Element of X : a \ b <= x3 } by Def5;

then ex x3 being Element of X st

( 0. X = x3 & a \ b <= x3 ) ;

then (a \ b) \ (0. X) = 0. X ;

then A3: a \ b = 0. X by Th2;

b in { xx where xx is Element of X : xx is atom } ;

then ex xx being Element of X st

( b = xx & xx is atom ) ;

hence contradiction by A1, A3; :: thesis: verum