let a, b be object ; :: according to RELAT_2:def 6,RELAT_2:def 14 :: 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

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