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

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

hence
for z being Element of Condition_S (x,y) holds z <= u
; :: thesis: verum
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;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