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

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