:: deftheorem defines Condition_S BCIALG_4:def 4 :
for X being BCI-Algebra_with_Condition(S)
for x, y being Element of X holds Condition_S (x,y) = { t where t is Element of X : t \ x <= y } ;