let X be set ; :: thesis: RelIncl X is transitive
let a be set ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: for b₁, b₂ being set holds
( not a in field (RelIncl X) or not b₁ in field (RelIncl X) or not b₂ in field (RelIncl X) or not [a,b₁] in RelIncl X or not [b₁,b₂] in RelIncl X or [a,b₂] in RelIncl X )
let b, c be set ; :: thesis: ( not a in field (RelIncl X) or not b in field (RelIncl X) or not c in field (RelIncl X) or not [a,b] in RelIncl X or not [b,c] in RelIncl X or [a,c] in RelIncl X )
assume A1: ( a in field (RelIncl X) & b in field (RelIncl X) & c in field (RelIncl X) & [a,b] in RelIncl X & [b,c] in RelIncl X ) ; :: thesis: [a,c] in RelIncl X
( field (RelIncl X) = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in RelIncl X iff Y c= Z ) ) ) by Def1;
then ( a c= b & b c= c ) by A1;
then ( a in X & c in X & a c= c ) by A1, Def1, XBOOLE_1:1;
hence [a,c] in RelIncl X by Def1; :: thesis: verum