let X be set ; :: thesis: for R being Relation holds
( R * (id X) c= R & (id X) * R c= R )
let R be Relation; :: thesis: ( R * (id X) c= R & (id X) * R c= R )
thus for x, y being object st [x,y] in R * (id X) holds
[x,y] in R :: according to RELAT_1:def 3 :: thesis: (id X) * R c= R

proof

let x, y be object ; :: thesis: ( [x,y] in R * (id X) implies [x,y] in R )
assume [x,y] in R * (id X) ; :: thesis: [x,y] in R
then ex z being object st
( [x,z] in R & [z,y] in id X ) by Def6;
hence [x,y] in R by Def8; :: thesis: verum

end;

thus for x, y being object st [x,y] in (id X) * R holds
[x,y] in R :: according to RELAT_1:def 3 :: thesis: verum

proof

let x, y be object ; :: thesis: ( [x,y] in (id X) * R implies [x,y] in R )
assume [x,y] in (id X) * R ; :: thesis: [x,y] in R
then ex z being object st
( [x,z] in id X & [z,y] in R ) by Def6;
hence [x,y] in R by Def8; :: thesis: verum

end;