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) = {}
b in { xx where xx is Element of X : xx is atom } ;
then consider xx being Element of X such that
A2: ( b = xx & xx is atom ) ;
assume (BranchV a) /\ (BranchV b) <> {} ; :: thesis: contradiction
then consider c being set such that
A3: c in (BranchV a) /\ (BranchV b) by XBOOLE_0:def 1;
reconsider z1 = c as Element of BranchV a by A3, XBOOLE_0:def 4;
reconsider z2 = c as Element of BranchV b by A3, 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 consider x3 being Element of X such that
A4: ( 0. X = x3 & a \ b <= x3 ) ;
(a \ b) \ (0. X) = 0. X by A4, Def11;
then a \ b = 0. X by Th2;
hence contradiction by A1, A2, Def14; :: thesis: verum