let X be non empty set ; :: thesis: for R being connected total Relation of X
for x, y being Element of X holds
( not x <> y or x,y in R or y,x in R )
let R be connected total Relation of X; :: thesis: for x, y being Element of X holds
( not x <> y or x,y in R or y,x in R )
let x, y be Element of X; :: thesis: ( not x <> y or x,y in R or y,x in R )
field R = X by ORDERS_1:12;
then ( not x <> y or [x,y] in R or [y,x] in R ) by RELAT_2:def 6, RELAT_2:def 14;
hence ( not x <> y or x,y in R or y,x in R ) ; :: thesis: verum