let x, y, z, t be set ; :: thesis: ( proj1 {[x,y],[z,t]} = {x,z} & proj2 {[x,y],[z,t]} = {y,t} )
( {[x,y],[z,t]} = {[x,y]} \/ {[z,t]} & {x,z} = {x} \/ {z} & {y,t} = {y} \/ {t} ) by ENUMSET1:41;
then ( proj1 {[x,y],[z,t]} = (proj1 {[x,y]}) \/ (proj1 {[z,t]}) & proj2 {[x,y],[z,t]} = (proj2 {[x,y]}) \/ (proj2 {[z,t]}) & proj1 {[x,y]} = {x} & proj1 {[z,t]} = {z} & proj2 {[x,y]} = {y} & proj2 {[z,t]} = {t} ) by Th6, Th15;
hence ( proj1 {[x,y],[z,t]} = {x,z} & proj2 {[x,y],[z,t]} = {y,t} ) by ENUMSET1:41; :: thesis: verum