let Y be set ; for R being Relation holds (R |_2 Y) |_2 Y = R |_2 Y
let R be Relation; (R |_2 Y) |_2 Y = R |_2 Y
let a, b be object ; RELAT_1:def 2 ( ( 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; ( not [a,b] in R |_2 Y or [a,b] in (R |_2 Y) |_2 Y )
assume A1:
[a,b] in R |_2 Y
; [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; verum