set O = the Order of {0};

take L = RelStr(# {0}, the Order of {0} #); :: thesis: L is connected

let x, y be Element of L; :: according to WAYBEL_0:def 29 :: thesis: ( x <= y or y <= x )

A1: x = 0 by TARSKI:def 1;

y = 0 by TARSKI:def 1;

hence ( x <= y or y <= x ) by A1, ORDERS_2:1; :: thesis: verum

take L = RelStr(# {0}, the Order of {0} #); :: thesis: L is connected

let x, y be Element of L; :: according to WAYBEL_0:def 29 :: thesis: ( x <= y or y <= x )

A1: x = 0 by TARSKI:def 1;

y = 0 by TARSKI:def 1;

hence ( x <= y or y <= x ) by A1, ORDERS_2:1; :: thesis: verum