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

(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