let a, b be Relation; :: thesis: a * b = a (#) b
thus a * b c= a (#) b :: according to XBOOLE_0:def 10 :: thesis: a (#) b c= a * b

proof

let x1, x2 be set ; :: according to RELAT_1:def 3 :: thesis: ( not [x1,x2] in a * b or [x1,x2] in a (#) b )
assume [x1,x2] in a * b ; :: thesis: [x1,x2] in a (#) b
then ex y being set st
( [x1,y] in a & [y,x2] in b ) by RELAT_1:def 8;
hence [x1,x2] in a (#) b by ZF_FUND1:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in a (#) b or x in a * b )
assume x in a (#) b ; :: thesis: x in a * b
then ex u, v, w being set st
( x = [u,w] & [u,v] in a & [v,w] in b ) by ZF_FUND1:def 1;
hence x in a * b by RELAT_1:def 8; :: thesis: verum