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 )

proof

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;

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