let X be BCI-Algebra_with_Condition(S); :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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) ; :: thesis: verum