Suggestion: Rename the attribute "connected"

We have

definition
 let L be non empty RelStr;
 attr L is connected means
:: WAYBEL_0:def 29

  for x,y being Element of L holds x <= y or y <= x;
end;

and also

definition let IT be RelStr;
  attr IT is disconnected  means
:: ORDERS_3:def 3  
   [#] IT is disconnected;
  antonym IT is connected;
end;

One of them should be renamed as (IMHO) the semantics is different

-- JosefUrban - 26 Jul 2002

Follow up