let A be Ordinal; :: thesis: RelIncl A is connected
let a be set ; :: according to RELAT_2:def 6,RELAT_2:def 14 :: thesis: for b₁ being set holds
( not a in field (RelIncl A) or not b₁ in field (RelIncl A) or a = b₁ or [a,b₁] in RelIncl A or [b₁,a] in RelIncl A )
let b be set ; :: thesis: ( not a in field (RelIncl A) or not b in field (RelIncl A) or a = b or [a,b] in RelIncl A or [b,a] in RelIncl A )
assume A1: ( a in field (RelIncl A) & b in field (RelIncl A) & a <> b ) ; :: thesis: ( [a,b] in RelIncl A or [b,a] in RelIncl A )
A2: ( field (RelIncl A) = A & ( for Y, Z being set st Y in A & Z in A holds
( [Y,Z] in RelIncl A iff Y c= Z ) ) ) by Def1;
then reconsider Y = a, Z = b as Ordinal by A1;
( Y c= Z or Z c= Y ) ;
hence ( [a,b] in RelIncl A or [b,a] in RelIncl A ) by A1, A2; :: thesis: verum