let X, Y be set ; ( Y c= X implies (RelIncl X) |_2 Y = RelIncl Y )
assume A1:
Y c= X
; (RelIncl X) |_2 Y = RelIncl Y
let a, b be object ; RELAT_1:def 2 ( ( 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 )
( not [a,b] in RelIncl Y or [a,b] in (RelIncl X) |_2 Y )proof
assume A2:
[a,b] in (RelIncl X) |_2 Y
;
[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;
verum
end;
assume A4:
[a,b] in RelIncl Y
; [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; verum