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