let o, p, q, r, s, t be set ; :: thesis: ( p <> r implies {[o,p],[q,r]} (#) {[p,s],[r,t]} = {[o,s],[q,t]} )
assume A1: p <> r ; :: thesis: {[o,p],[q,r]} (#) {[p,s],[r,t]} = {[o,s],[q,t]}
let a1, a3 be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]} or [a1,a3] in {[o,s],[q,t]} ) & ( not [a1,a3] in {[o,s],[q,t]} or [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]} ) )
thus ( [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]} implies [a1,a3] in {[o,s],[q,t]} ) :: thesis: ( not [a1,a3] in {[o,s],[q,t]} or [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]} )

proof

assume [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]} ; :: thesis: [a1,a3] in {[o,s],[q,t]}
then consider a2 being object such that
A2: [a1,a2] in {[o,p],[q,r]} and
A3: [a2,a3] in {[p,s],[r,t]} by RELAT_1:def 8;
( [a1,a2] = [o,p] or [a1,a2] = [q,r] ) by A2, TARSKI:def 2;
then A4: ( ( a1 = o & a2 = p ) or ( a1 = q & a2 = r ) ) by XTUPLE_0:1;
( [a2,a3] = [p,s] or [a2,a3] = [r,t] ) by A3, TARSKI:def 2;
then ( ( a1 = o & a2 = p & a3 = s ) or ( a1 = q & a2 = r & a3 = t ) ) by A1, A4, XTUPLE_0:1;
hence [a1,a3] in {[o,s],[q,t]} by TARSKI:def 2; :: thesis: verum

end;

assume A5: [a1,a3] in {[o,s],[q,t]} ; :: thesis: [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]}

per cases ( [a1,a3] = [o,s] or [a1,a3] = [q,t] ) by A5, TARSKI:def 2;

suppose A6: [a1,a3] = [o,s] ; :: thesis: [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]}

( [o,p] in {[o,p],[q,r]} & [p,s] in {[p,s],[r,t]} ) by TARSKI:def 2;
hence [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]} by A6, RELAT_1:def 8; :: thesis: verum

end;

suppose A7: [a1,a3] = [q,t] ; :: thesis: [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]}

( [q,r] in {[o,p],[q,r]} & [r,t] in {[p,s],[r,t]} ) by TARSKI:def 2;
hence [a1,a3] in {[o,p],[q,r]} (#) {[p,s],[r,t]} by A7, RELAT_1:def 8; :: thesis: verum

end;

end;