let X be BCI-Algebra_with_Condition(S); :: thesis: for x, y being Element of X ex a being Element of Condition_S (x,y) st
for z being Element of Condition_S (x,y) holds z <= a
let x, y be Element of X; :: thesis: ex a being Element of Condition_S (x,y) st
for z being Element of Condition_S (x,y) holds z <= a
((x * y) \ x) \ y = (x * y) \ (x * y) by Def2
.= 0. X by BCIALG_1:def 5 ;
then (x * y) \ x <= y ;
then x * y in { t where t is Element of X : t \ x <= y } ;
then consider u being Element of Condition_S (x,y) such that
A1: u = x * y ;
take u ; :: thesis: for z being Element of Condition_S (x,y) holds z <= u
for z being Element of Condition_S (x,y) holds z <= u

proof

let z be Element of Condition_S (x,y); :: thesis: z <= u
z in { t where t is Element of X : t \ x <= y } ;
then consider z1 being Element of X such that
A2: z = z1 and
A3: z1 \ x <= y ;
z \ u = (z1 \ x) \ y by A1, A2, Def2
.= 0. X by A3 ;
hence z <= u ; :: thesis: verum

end;

hence for z being Element of Condition_S (x,y) holds z <= u ; :: thesis: verum