:: deftheorem Def2 defines with_condition_S BCIALG_4:def 2 :
for IT being non empty BCIStr_1 holds
( IT is with_condition_S iff for x, y, z being Element of IT holds (x \ y) \ z = x \ (y * z) );