A1: field (RelIncl X) = X by Def1;
let a be object ; :: according to RELAT_2:def 1,RELAT_2:def 9 :: thesis: ( not a in field (RelIncl X) or [a,a] in RelIncl X )
assume a in field (RelIncl X) ; :: thesis: [a,a] in RelIncl X
hence [a,a] in RelIncl X by A1, Def1; :: thesis: verum