let A be set ; :: thesis: for Q, R being Relation st Q | A = R | A holds
Q .: A = R .: A
let Q, R be Relation; :: thesis: ( Q | A = R | A implies Q .: A = R .: A )
assume Q | A = R | A ; :: thesis: Q .: A = R .: A
hence Q .: A = (R | A) .: A by Th121
.= R .: A by Th121 ;
:: thesis: verum