let R be Relation; :: thesis: for A, B, C being set st A c= B & A c= C holds
(R | B) | A = (R | C) | A
let A, B, C be set ; :: thesis: ( A c= B & A c= C implies (R | B) | A = (R | C) | A )
assume that
A1: A c= B and
A2: A c= C ; :: thesis: (R | B) | A = (R | C) | A
(R | C) | A = R | A by A2, RELAT_1:74;
hence (R | B) | A = (R | C) | A by A1, RELAT_1:74; :: thesis: verum