let Y be set ; :: thesis: for R being Relation holds (R |_2 Y) |_2 Y = R |_2 Y

let R be Relation; :: thesis: (R |_2 Y) |_2 Y = R |_2 Y

let a, b be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,b] in (R |_2 Y) |_2 Y or [a,b] in R |_2 Y ) & ( not [a,b] in R |_2 Y or [a,b] in (R |_2 Y) |_2 Y ) )

thus ( [a,b] in (R |_2 Y) |_2 Y implies [a,b] in R |_2 Y ) by XBOOLE_0:def 4; :: thesis: ( not [a,b] in R |_2 Y or [a,b] in (R |_2 Y) |_2 Y )

assume A1: [a,b] in R |_2 Y ; :: thesis: [a,b] in (R |_2 Y) |_2 Y

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

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

let R be Relation; :: thesis: (R |_2 Y) |_2 Y = R |_2 Y

let a, b be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,b] in (R |_2 Y) |_2 Y or [a,b] in R |_2 Y ) & ( not [a,b] in R |_2 Y or [a,b] in (R |_2 Y) |_2 Y ) )

thus ( [a,b] in (R |_2 Y) |_2 Y implies [a,b] in R |_2 Y ) by XBOOLE_0:def 4; :: thesis: ( not [a,b] in R |_2 Y or [a,b] in (R |_2 Y) |_2 Y )

assume A1: [a,b] in R |_2 Y ; :: thesis: [a,b] in (R |_2 Y) |_2 Y

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

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