let X be BCI-Algebra_with_Condition(S); for x, y, u, v being Element of X st u in Condition_S (x,y) & v <= u holds
v in Condition_S (x,y)
let x, y, u, v be Element of X; ( u in Condition_S (x,y) & v <= u implies v in Condition_S (x,y) )
assume that
A1:
u in Condition_S (x,y)
and
A2:
v <= u
; v in Condition_S (x,y)
v \ x <= u \ x
by A2, BCIALG_1:5;
then A3:
(v \ x) \ (u \ x) = 0. X
;
ex u1 being Element of X st
( u = u1 & u1 \ x <= y )
by A1;
then
(u \ x) \ y = 0. X
;
then
(v \ x) \ y = 0. X
by A3, BCIALG_1:3;
then
v \ x <= y
;
hence
v in Condition_S (x,y)
; verum