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
ex a being Element of Condition_S (x,y) st
for z being Element of Condition_S (x,y) holds z <= a

proof

(x * y) \ x <= y by Lm2;
then x * y in Condition_S (x,y) ;
then consider a being Element of Condition_S (x,y) such that
A1: a = x * y ;
take a ; :: thesis: for z being Element of Condition_S (x,y) holds z <= a
for t1 being Element of Condition_S (x,y) holds t1 <= a

proof

let t1 be Element of Condition_S (x,y); :: thesis: t1 <= a
t1 in { t where t is Element of X : t \ x <= y } ;
then ex t2 being Element of X st
( t2 = t1 & t2 \ x <= y ) ;
hence t1 <= a by A1, Lm2; :: thesis: verum

end;

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

end;

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