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