let X, Y be set ; :: thesis: ( Y c= X implies () |_2 Y = RelIncl Y )
assume A1: Y c= X ; :: thesis: () |_2 Y = RelIncl Y
let a, b be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,b] in () |_2 Y or [a,b] in RelIncl Y ) & ( not [a,b] in RelIncl Y or [a,b] in () |_2 Y ) )
thus ( [a,b] in () |_2 Y implies [a,b] in RelIncl Y ) :: thesis: ( not [a,b] in RelIncl Y or [a,b] in () |_2 Y )
proof
assume A2: [a,b] in () |_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 ;
then a c= b by A1, A3, Def1;
hence [a,b] in RelIncl Y by ; :: thesis: verum
end;
assume A4: [a,b] in RelIncl Y ; :: thesis: [a,b] in () |_2 Y
then A5: ( a in field () & b in field () ) by RELAT_1:15;
reconsider a = a, b = b as set by TARSKI:1;
A6: field () = 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 ;
hence [a,b] in () |_2 Y by ; :: thesis: verum