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

for y being Element of BranchV b holds y <= mb ; :: thesis: verum

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

hence
ex mb being Element of X st
set mb = (b * ((0. X) \ a)) * ma;

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

for y being Element of BranchV b holds y <= mb ; :: thesis: verum

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

proof

hence
ex mb being Element of X st
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;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

for y being Element of BranchV b holds y <= mb ; :: thesis: verum

for y being Element of BranchV b holds y <= mb ; :: thesis: verum