let X be set ; :: thesis: Total X is connected
let x be set ; :: according to RELAT_2:def 6,RELAT_2:def 14 :: thesis: for b₁ being set holds
( not x in field (Total X) or not b₁ in field (Total X) or x = b₁ or [x,b₁] in Total X or [b₁,x] in Total X )
let y be set ; :: thesis: ( not x in field (Total X) or not y in field (Total X) or x = y or [x,y] in Total X or [y,x] in Total X )
assume that
A1: ( x in field (Total X) & y in field (Total X) ) and
x <> y ; :: thesis: ( [x,y] in Total X or [y,x] in Total X )
( x in X & y in X ) by A1, ORDERS_1:12;
then [x,y] in [:X,X:] by ZFMISC_1:87;
hence ( [x,y] in Total X or [y,x] in Total X ) by EQREL_1:def 1; :: thesis: verum