let o, p, q be set ; :: thesis: {[o,p],[p,p]} (#) {[p,q]} = {[o,q],[p,q]}
let s, u be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [s,u] in {[o,p],[p,p]} (#) {[p,q]} or [s,u] in {[o,q],[p,q]} ) & ( not [s,u] in {[o,q],[p,q]} or [s,u] in {[o,p],[p,p]} (#) {[p,q]} ) )
thus ( [s,u] in {[o,p],[p,p]} (#) {[p,q]} implies [s,u] in {[o,q],[p,q]} ) :: thesis: ( not [s,u] in {[o,q],[p,q]} or [s,u] in {[o,p],[p,p]} (#) {[p,q]} )
proof
assume [s,u] in {[o,p],[p,p]} (#) {[p,q]} ; :: thesis: [s,u] in {[o,q],[p,q]}
then consider t being object such that
A1: [s,t] in {[o,p],[p,p]} and
A2: [t,u] in {[p,q]} by RELAT_1:def 8;
[t,u] = [p,q] by A2, TARSKI:def 1;
then A3: u = q by XTUPLE_0:1;
( [s,t] = [o,p] or [s,t] = [p,p] ) by A1, TARSKI:def 2;
then ( [s,u] = [o,q] or [s,u] = [p,q] ) by A3, XTUPLE_0:1;
hence [s,u] in {[o,q],[p,q]} by TARSKI:def 2; :: thesis: verum
end;
assume A4: [s,u] in {[o,q],[p,q]} ; :: thesis: [s,u] in {[o,p],[p,p]} (#) {[p,q]}
per cases ( [s,u] = [o,q] or [s,u] = [p,q] ) by A4, TARSKI:def 2;
suppose A5: [s,u] = [o,q] ; :: thesis: [s,u] in {[o,p],[p,p]} (#) {[p,q]}
( [o,p] in {[o,p],[p,p]} & [p,q] in {[p,q]} ) by TARSKI:def 1, TARSKI:def 2;
hence [s,u] in {[o,p],[p,p]} (#) {[p,q]} by A5, RELAT_1:def 8; :: thesis: verum
end;
suppose A6: [s,u] = [p,q] ; :: thesis: [s,u] in {[o,p],[p,p]} (#) {[p,q]}
( [p,p] in {[o,p],[p,p]} & [p,q] in {[p,q]} ) by TARSKI:def 1, TARSKI:def 2;
hence [s,u] in {[o,p],[p,p]} (#) {[p,q]} by A6, RELAT_1:def 8; :: thesis: verum
end;
end;