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 be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( 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 ) )
let b be set ; :: 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