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 by BCIALG_1:def 11;
ex u1 being Element of X st
( u = u1 & u1 \ x <= y ) by A1;
then (u \ x) \ y = 0. X by BCIALG_1:def 11;
then (v \ x) \ y = 0. X by A3, BCIALG_1:3;
then v \ x <= y by BCIALG_1:def 11;
hence v in Condition_S x,y ; :: thesis: verum