let o, p, q, r, s, t be set ; ( p <> r implies {[o,p],[q,r]} (#) {[p,s],[r,t]} = {[o,s],[q,t]} )
assume A1:
p <> r
; {[o,p],[q,r]} (#) {[p,s],[r,t]} = {[o,s],[q,t]}
let a1, a3 be object ; RELAT_1:def 2 ( ( 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]} )
( 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]}
;
[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;
verum
end;
assume A5:
[a1,a3] in {[o,s],[q,t]}
; [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]
;
[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;
verum suppose A7:
[a1,a3] = [q,t]
;
[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;
verum