let X be commutative BCK-Algebra_with_Condition(S); :: thesis: for a, b, c being Element of X st Condition_S (a,b) c= Initial_section c holds

for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b)

let a, b, c be Element of X; :: thesis: ( Condition_S (a,b) c= Initial_section c implies for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b) )

assume A1: Condition_S (a,b) c= Initial_section c ; :: thesis: for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b)

for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b)

for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b)

let a, b, c be Element of X; :: thesis: ( Condition_S (a,b) c= Initial_section c implies for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b) )

assume A1: Condition_S (a,b) c= Initial_section c ; :: thesis: for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b)

for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b)

proof

hence
for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b)
; :: thesis: verum
set u = c \ ((c \ a) \ b);

let x be Element of Condition_S (a,b); :: thesis: x <= c \ ((c \ a) \ b)

A2: (c \ (c \ x)) \ x = (c \ x) \ (c \ x) by BCIALG_1:7

.= 0. X by BCIALG_1:def 5 ;

x in { t2 where t2 is Element of X : t2 <= c } by A1, TARSKI:def 3;

then consider x2 being Element of X such that

A3: x = x2 and

A4: x2 <= c ;

A5: x \ (c \ (c \ x)) = x \ (x \ (x \ c)) by Def9

.= x2 \ c by A3, BCIALG_1:8

.= 0. X by A4 ;

then A6: ( ((c \ (c \ x)) \ (c \ ((c \ a) \ b))) \ (((c \ a) \ b) \ (c \ x)) = 0. X & x \ (c \ ((c \ a) \ b)) = (c \ (c \ x)) \ (c \ ((c \ a) \ b)) ) by A2, BCIALG_1:1, BCIALG_1:def 7;

x in { t1 where t1 is Element of X : t1 \ a <= b } ;

then A7: ex x1 being Element of X st

( x = x1 & x1 \ a <= b ) ;

((c \ a) \ b) \ (c \ x) = ((c \ a) \ (c \ x)) \ b by BCIALG_1:7

.= ((c \ (c \ x)) \ a) \ b by BCIALG_1:7

.= (x \ a) \ b by A5, A2, BCIALG_1:def 7

.= 0. X by A7 ;

then x \ (c \ ((c \ a) \ b)) = 0. X by A6, BCIALG_1:2;

hence x <= c \ ((c \ a) \ b) ; :: thesis: verum

end;let x be Element of Condition_S (a,b); :: thesis: x <= c \ ((c \ a) \ b)

A2: (c \ (c \ x)) \ x = (c \ x) \ (c \ x) by BCIALG_1:7

.= 0. X by BCIALG_1:def 5 ;

x in { t2 where t2 is Element of X : t2 <= c } by A1, TARSKI:def 3;

then consider x2 being Element of X such that

A3: x = x2 and

A4: x2 <= c ;

A5: x \ (c \ (c \ x)) = x \ (x \ (x \ c)) by Def9

.= x2 \ c by A3, BCIALG_1:8

.= 0. X by A4 ;

then A6: ( ((c \ (c \ x)) \ (c \ ((c \ a) \ b))) \ (((c \ a) \ b) \ (c \ x)) = 0. X & x \ (c \ ((c \ a) \ b)) = (c \ (c \ x)) \ (c \ ((c \ a) \ b)) ) by A2, BCIALG_1:1, BCIALG_1:def 7;

x in { t1 where t1 is Element of X : t1 \ a <= b } ;

then A7: ex x1 being Element of X st

( x = x1 & x1 \ a <= b ) ;

((c \ a) \ b) \ (c \ x) = ((c \ a) \ (c \ x)) \ b by BCIALG_1:7

.= ((c \ (c \ x)) \ a) \ b by BCIALG_1:7

.= (x \ a) \ b by A5, A2, BCIALG_1:def 7

.= 0. X by A7 ;

then x \ (c \ ((c \ a) \ b)) = 0. X by A6, BCIALG_1:2;

hence x <= c \ ((c \ a) \ b) ; :: thesis: verum