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)

proof

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;

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