theorem :: BCIALG_4:1

for X being 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)