let L be non empty reflexive RelStr ; :: thesis: ( L is trivial implies L is connected )

assume A1: for x, y being Element of L holds x = y ; :: according to STRUCT_0:def 10 :: thesis: L is connected

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

z1 = z2 by A1;

hence ( z1 <= z2 or z2 <= z1 ) by ORDERS_2:1; :: thesis: verum

assume A1: for x, y being Element of L holds x = y ; :: according to STRUCT_0:def 10 :: thesis: L is connected

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

z1 = z2 by A1;

hence ( z1 <= z2 or z2 <= z1 ) by ORDERS_2:1; :: thesis: verum