let X be BCK-Algebra_with_Condition(S); :: thesis: for x, y being Element of X holds

( x <= x * y & y <= x * y )

for x, y being Element of X holds

( x <= x * y & y <= x * y )

( x <= x * y & y <= x * y ) ; :: thesis: verum

( x <= x * y & y <= x * y )

for x, y being Element of X holds

( x <= x * y & y <= x * y )

proof

hence
for x, y being Element of X holds
let x, y be Element of X; :: thesis: ( x <= x * y & y <= x * y )

A1: (x \ x) \ y = y ` by BCIALG_1:def 5

.= 0. X by BCIALG_1:def 8 ;

A2: (y \ y) \ x = x ` by BCIALG_1:def 5

.= 0. X by BCIALG_1:def 8 ;

A3: (x \ x) \ y = x \ (x * y) by Th11;

(y \ y) \ x = y \ (y * x) by Th11

.= y \ (x * y) by Th6 ;

hence ( x <= x * y & y <= x * y ) by A3, A1, A2; :: thesis: verum

end;A1: (x \ x) \ y = y ` by BCIALG_1:def 5

.= 0. X by BCIALG_1:def 8 ;

A2: (y \ y) \ x = x ` by BCIALG_1:def 5

.= 0. X by BCIALG_1:def 8 ;

A3: (x \ x) \ y = x \ (x * y) by Th11;

(y \ y) \ x = y \ (y * x) by Th11

.= y \ (x * y) by Th6 ;

hence ( x <= x * y & y <= x * y ) by A3, A1, A2; :: thesis: verum

( x <= x * y & y <= x * y ) ; :: thesis: verum