let Y, X be set ; :: thesis: ( Y c= X implies (RelIncl X) |_2 Y = RelIncl Y )
assume A1: Y c= X ; :: thesis: (RelIncl X) |_2 Y = RelIncl Y
let a be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( not [a,b₁] in (RelIncl X) |_2 Y or [a,b₁] in RelIncl Y ) & ( not [a,b₁] in RelIncl Y or [a,b₁] in (RelIncl X) |_2 Y ) )
let b be set ; :: thesis: ( ( not [a,b] in (RelIncl X) |_2 Y or [a,b] in RelIncl Y ) & ( not [a,b] in RelIncl Y or [a,b] in (RelIncl X) |_2 Y ) )
thus ( [a,b] in (RelIncl X) |_2 Y implies [a,b] in RelIncl Y ) :: thesis: ( not [a,b] in RelIncl Y or [a,b] in (RelIncl X) |_2 Y )

proof

assume [a,b] in (RelIncl X) |_2 Y ; :: thesis: [a,b] in RelIncl Y
then A2: ( [a,b] in [:Y,Y:] & [a,b] in RelIncl X ) by XBOOLE_0:def 4;
then A3: ( a in Y & b in Y ) by ZFMISC_1:106;
then a c= b by A1, A2, Def1;
hence [a,b] in RelIncl Y by A3, Def1; :: thesis: verum

end;

assume A4: [a,b] in RelIncl Y ; :: thesis: [a,b] in (RelIncl X) |_2 Y
then A5: ( a in field (RelIncl Y) & b in field (RelIncl Y) & field (RelIncl Y) = Y ) by Def1, RELAT_1:30;
then a c= b by A4, Def1;
then ( [a,b] in RelIncl X & [a,b] in [:Y,Y:] ) by A1, A5, Def1, ZFMISC_1:106;
hence [a,b] in (RelIncl X) |_2 Y by XBOOLE_0:def 4; :: thesis: verum