let p, r, o, q, 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]}
thus {[o,p],[q,r]} (#) {[p,s],[r,t]} c= {[o,s],[q,t]} :: according to XBOOLE_0:def 10 :: thesis: {[o,s],[q,t]} c= {[o,p],[q,r]} (#) {[p,s],[r,t]}

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in {[o,p],[q,r]} (#) {[p,s],[r,t]} or u in {[o,s],[q,t]} )
assume u in {[o,p],[q,r]} (#) {[p,s],[r,t]} ; :: thesis: u in {[o,s],[q,t]}
then consider a1, a2, a3 being set such that
A2: ( u = [a1,a3] & [a1,a2] in {[o,p],[q,r]} & [a2,a3] in {[p,s],[r,t]} ) by Def1;
( [a1,a2] = [o,p] or [a1,a2] = [q,r] ) by A2, TARSKI:def 2;
then A3: ( ( a1 = o & a2 = p ) or ( a1 = q & a2 = r ) ) by ZFMISC_1:33;
( [a2,a3] = [p,s] or [a2,a3] = [r,t] ) by A2, TARSKI:def 2;
then ( ( a1 = o & a2 = p & a3 = s ) or ( a1 = q & a2 = r & a3 = t ) ) by A1, A3, ZFMISC_1:33;
hence u in {[o,s],[q,t]} by A2, TARSKI:def 2; :: thesis: verum

end;

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in {[o,s],[q,t]} or u in {[o,p],[q,r]} (#) {[p,s],[r,t]} )
assume A4: u in {[o,s],[q,t]} ; :: thesis: u in {[o,p],[q,r]} (#) {[p,s],[r,t]}

per cases ( u = [o,s] or u = [q,t] ) by A4, TARSKI:def 2;

suppose A5: u = [o,s] ; :: thesis: u 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 u in {[o,p],[q,r]} (#) {[p,s],[r,t]} by A5, Def1; :: thesis: verum

end;

suppose A6: u = [q,t] ; :: thesis: u 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 u in {[o,p],[q,r]} (#) {[p,s],[r,t]} by A6, Def1; :: thesis: verum

end;

end;