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] & [s,t] in {[o,p],[p,p]} & [t,u] in {[p,q]} ) by Def1;
[t,u] = [p,q] by A1, TARSKI:def 1;
then A2: u = q by ZFMISC_1:33;
( [s,t] = [o,p] or [s,t] = [p,p] ) by A1, TARSKI:def 2;
then ( r = [o,q] or r = [p,q] ) by A1, A2, ZFMISC_1:33;
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 A3: 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 A3, TARSKI:def 2;

suppose A4: r = [o,q] ; :: thesis: r in {[o,p],[p,p]} (#) {[p,q]}

A5: [o,p] in {[o,p],[p,p]} by TARSKI:def 2;
[p,q] in {[p,q]} by TARSKI:def 1;
hence r in {[o,p],[p,p]} (#) {[p,q]} by A4, A5, Def1; :: thesis: verum

end;

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

A7: [p,p] in {[o,p],[p,p]} by TARSKI:def 2;
[p,q] in {[p,q]} by TARSKI:def 1;
hence r in {[o,p],[p,p]} (#) {[p,q]} by A6, A7, Def1; :: thesis: verum

end;

end;