let o, p, q be set ; :: thesis: {[o,p],[p,p]} (#) {[p,q]} = {[o,q],[p,q]}
thus {[o,p],[p,p]} (#) {[p,q]} c= {[o,q],[p,q]} :: according to XBOOLE_0:def 10 :: thesis: {[o,q],[p,q]} c= {[o,p],[p,p]} (#) {[p,q]}

proof

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

end;

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

per cases ( r = [o,q] or r = [p,q] ) by A5, TARSKI:def 2;

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

end;

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

end;

end;