let x, y be object ; :: thesis: ( proj1 {[x,y]} = {x} & proj2 {[x,y]} = {y} )
thus proj1 {[x,y]} c= {x} :: according to XBOOLE_0:def 10 :: thesis: ( {x} c= proj1 {[x,y]} & proj2 {[x,y]} = {y} )
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in proj1 {[x,y]} or z in {x} )
assume z in proj1 {[x,y]} ; :: thesis: z in {x}
then consider t being object such that
A1: [z,t] in {[x,y]} by XTUPLE_0:def 12;
[z,t] = [x,y] by A1, TARSKI:def 1;
then z = x by XTUPLE_0:1;
hence z in {x} by TARSKI:def 1; :: thesis: verum
end;
thus {x} c= proj1 {[x,y]} :: thesis: proj2 {[x,y]} = {y}
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {x} or z in proj1 {[x,y]} )
assume z in {x} ; :: thesis: z in proj1 {[x,y]}
then z = x by TARSKI:def 1;
then [z,y] in {[x,y]} by TARSKI:def 1;
hence z in proj1 {[x,y]} by XTUPLE_0:def 12; :: thesis: verum
end;
thus proj2 {[x,y]} c= {y} :: according to XBOOLE_0:def 10 :: thesis: {y} c= proj2 {[x,y]}
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in proj2 {[x,y]} or z in {y} )
assume z in proj2 {[x,y]} ; :: thesis: z in {y}
then consider t being object such that
A2: [t,z] in {[x,y]} by XTUPLE_0:def 13;
[t,z] = [x,y] by A2, TARSKI:def 1;
then z = y by XTUPLE_0:1;
hence z in {y} by TARSKI:def 1; :: thesis: verum
end;
thus {y} c= proj2 {[x,y]} :: thesis: verum
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {y} or z in proj2 {[x,y]} )
assume z in {y} ; :: thesis: z in proj2 {[x,y]}
then z = y by TARSKI:def 1;
then [x,z] in {[x,y]} by TARSKI:def 1;
hence z in proj2 {[x,y]} by XTUPLE_0:def 13; :: thesis: verum
end;