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