consider O being Order of {0 };
take L = RelStr(# {0 },O #); :: thesis: L is connected
let x, y be Element of L; :: according to WAYBEL_0:def 29 :: thesis: ( x <= y or y <= x )
( x = 0 & y = 0 ) by TARSKI:def 1;
hence ( x <= y or y <= x ) by ORDERS_2:24; :: thesis: verum