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 that
A1: a in field (RelIncl X) and
A2: b in field (RelIncl X) and
A3: c in field (RelIncl X) and
A4: ( [a,b] in RelIncl X & [b,c] in RelIncl X ) ; :: thesis: [a,c] in RelIncl X
field (RelIncl X) = X by Def1;
then ( a c= b & b c= c ) by A1, A2, A3, A4, Def1;
then A5: a c= c by XBOOLE_1:1;
( a in X & c in X ) by A1, A3, Def1;
hence [a,c] in RelIncl X by A5, Def1; :: thesis: verum