let R be non empty real RelStr ; :: thesis: R is connected
let x, y be Element of R; :: according to WAYBEL_0:def 29 :: thesis: ( x <<= y or y <<= x )
( x <= y or x >= y ) ;
hence ( x <<= y or y <<= x ) by Th3; :: thesis: verum