let X be BCI-Algebra_with_Condition(S); :: thesis: for a, b being Element of AtomSet X
for ma being Element of X st ( for x being Element of BranchV a holds x <= ma ) holds
ex mb being Element of X st
for y being Element of BranchV b holds y <= mb
let a, b be Element of AtomSet X; :: thesis: for ma being Element of X st ( for x being Element of BranchV a holds x <= ma ) holds
ex mb being Element of X st
for y being Element of BranchV b holds y <= mb
let ma be Element of X; :: thesis: ( ( for x being Element of BranchV a holds x <= ma ) implies ex mb being Element of X st
for y being Element of BranchV b holds y <= mb )
assume A1: for x being Element of BranchV a holds x <= ma ; :: thesis: ex mb being Element of X st
for y being Element of BranchV b holds y <= mb
ex mb being Element of X st
for y being Element of BranchV b holds y <= mb

proof

set mb = (b * ((0. X) \ a)) * ma;
for y being Element of BranchV b holds y <= (b * ((0. X) \ a)) * ma

proof

a \ a = 0. X by BCIALG_1:def 5;
then a <= a ;
then a in { yy2 where yy2 is Element of X : a <= yy2 } ;
then A2: a is Element of BranchV a ;
let y be Element of BranchV b; :: thesis: y <= (b * ((0. X) \ a)) * ma
0. X in AtomSet X ;
then consider x0 being Element of AtomSet X such that
A3: x0 = 0. X ;
y in { yy where yy is Element of X : b <= yy } ;
then ex yy being Element of X st
( y = yy & b <= yy ) ;
then b \ b <= y \ b by BCIALG_1:5;
then y \ b in { yy1 where yy1 is Element of X : b \ b <= yy1 } ;
then A4: y \ b is Element of BranchV (b \ b) ;
A5: (b \ b) \ (x0 \ a) = x0 \ (x0 \ a) by A3, BCIALG_1:def 5
.= a by BCIALG_1:24 ;
x0 \ x0 = 0. X by BCIALG_1:def 5;
then x0 <= x0 ;
then x0 in { yy2 where yy2 is Element of X : x0 <= yy2 } ;
then x0 is Element of BranchV x0 ;
then x0 \ a is Element of BranchV (x0 \ a) by A2, BCIALG_1:39;
then (y \ b) \ (x0 \ a) is Element of BranchV a by A4, A5, BCIALG_1:39;
then A6: (y \ b) \ (x0 \ a) <= ma by A1;
y \ ((b * ((0. X) \ a)) * ma) = (y \ (b * ((0. X) \ a))) \ ma by Th11
.= ((y \ b) \ (x0 \ a)) \ ma by A3, Th11
.= 0. X by A6 ;
hence y <= (b * ((0. X) \ a)) * ma ; :: thesis: verum

end;

hence ex mb being Element of X st
for y being Element of BranchV b holds y <= mb ; :: thesis: verum

end;

hence ex mb being Element of X st
for y being Element of BranchV b holds y <= mb ; :: thesis: verum