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 that
A1: ( a in field (RelIncl A) & b in field (RelIncl A) ) and
a <> b ; :: thesis: ( [a,b] in RelIncl A or [b,a] in RelIncl A )
A2: field (RelIncl A) = A 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, Def1; :: thesis: verum