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
let x be
Element of
Condition_S a,
b;
:: thesis: x <= c \ ((c \ a) \ b)
set u =
c \ ((c \ a) \ b);
x in { t1 where t1 is Element of X : t1 \ a <= b }
;
then consider x1 being
Element of
X such that A2:
(
x = x1 &
x1 \ a <= b )
;
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 &
x2 <= c )
;
A4:
x \ (c \ (c \ x)) =
x \ (x \ (x \ c))
by Def9
.=
x2 \ c
by A3, BCIALG_1:8
.=
0. X
by A3, BCIALG_1:def 11
;
A5:
(c \ (c \ x)) \ x =
(c \ x) \ (c \ x)
by BCIALG_1:7
.=
0. X
by BCIALG_1:def 5
;
A6:
((c \ (c \ x)) \ (c \ ((c \ a) \ b))) \ (((c \ a) \ b) \ (c \ x)) = 0. X
by BCIALG_1:1;
A7:
((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 A4, A5, BCIALG_1:def 7
.=
0. X
by A2, BCIALG_1:def 11
;
x \ (c \ ((c \ a) \ b)) = (c \ (c \ x)) \ (c \ ((c \ a) \ b))
by A4, A5, BCIALG_1:def 7;
then
x \ (c \ ((c \ a) \ b)) = 0. X
by A6, A7, BCIALG_1:2;
hence
x <= c \ ((c \ a) \ b)
by BCIALG_1:def 11;
:: thesis: verum
end;
hence
for x being Element of Condition_S a,b holds x <= c \ ((c \ a) \ b)
; :: thesis: verum