let X, Y 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, b be object ; :: according to RELAT_1:def 2 :: 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 )

then A5: ( a in field (RelIncl Y) & b in field (RelIncl Y) ) by RELAT_1:15;

reconsider a = a, b = b as set by TARSKI:1;

A6: field (RelIncl Y) = Y by Def1;

then a c= b by A4, A5, Def1;

then A7: [a,b] in RelIncl X by A1, A5, A6, Def1;

[a,b] in [:Y,Y:] by A5, A6, ZFMISC_1:87;

hence [a,b] in (RelIncl X) |_2 Y by A7, XBOOLE_0:def 4; :: thesis: verum

assume A1: Y c= X ; :: thesis: (RelIncl X) |_2 Y = RelIncl Y

let a, b be object ; :: according to RELAT_1:def 2 :: 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 A4:
[a,b] in RelIncl Y
; :: thesis: [a,b] in (RelIncl X) |_2 Y
assume A2:
[a,b] in (RelIncl X) |_2 Y
; :: thesis: [a,b] in RelIncl Y

then [a,b] in [:Y,Y:] by XBOOLE_0:def 4;

then A3: ( a in Y & b in Y ) by ZFMISC_1:87;

reconsider a = a, b = b as set by TARSKI:1;

[a,b] in RelIncl X by A2, XBOOLE_0:def 4;

then a c= b by A1, A3, Def1;

hence [a,b] in RelIncl Y by A3, Def1; :: thesis: verum

end;then [a,b] in [:Y,Y:] by XBOOLE_0:def 4;

then A3: ( a in Y & b in Y ) by ZFMISC_1:87;

reconsider a = a, b = b as set by TARSKI:1;

[a,b] in RelIncl X by A2, XBOOLE_0:def 4;

then a c= b by A1, A3, Def1;

hence [a,b] in RelIncl Y by A3, Def1; :: thesis: verum

then A5: ( a in field (RelIncl Y) & b in field (RelIncl Y) ) by RELAT_1:15;

reconsider a = a, b = b as set by TARSKI:1;

A6: field (RelIncl Y) = Y by Def1;

then a c= b by A4, A5, Def1;

then A7: [a,b] in RelIncl X by A1, A5, A6, Def1;

[a,b] in [:Y,Y:] by A5, A6, ZFMISC_1:87;

hence [a,b] in (RelIncl X) |_2 Y by A7, XBOOLE_0:def 4; :: thesis: verum