now :: thesis: for x, y being object st x in field (RelIncl X) & y in field (RelIncl X) & x <> y & not [x,y] in RelIncl X holds
[y,x] in RelIncl X

let x, y be object ; :: thesis: ( x in field (RelIncl X) & y in field (RelIncl X) & x <> y & not [b₁,b₂] in RelIncl X implies [b₂,b₁] in RelIncl X )
assume ( x in field (RelIncl X) & y in field (RelIncl X) & x <> y ) ; :: thesis: ( [b₁,b₂] in RelIncl X or [b₂,b₁] in RelIncl X )
then A1: ( x in X & y in X ) by WELLORD2:def 1;
reconsider A = x, B = y as set by TARSKI:1;

per cases ( A c= B or B c= A ) by A1, ORDINAL1:def 8, XBOOLE_0:def 9;

suppose A c= B ; :: thesis: ( [b₁,b₂] in RelIncl X or [b₂,b₁] in RelIncl X )

hence ( [x,y] in RelIncl X or [y,x] in RelIncl X ) by A1, WELLORD2:def 1; :: thesis: verum

end;

suppose B c= A ; :: thesis: ( [b₁,b₂] in RelIncl X or [b₂,b₁] in RelIncl X )

hence ( [x,y] in RelIncl X or [y,x] in RelIncl X ) by A1, WELLORD2:def 1; :: thesis: verum

end;

end;

end;

hence RelIncl X is connected by RELAT_2:def 6, RELAT_2:def 14; :: thesis: verum