let x, y be object ; ( proj1 {[x,y]} = {x} & proj2 {[x,y]} = {y} )
thus
proj1 {[x,y]} c= {x}
XBOOLE_0:def 10 ( {x} c= proj1 {[x,y]} & proj2 {[x,y]} = {y} )
thus
{x} c= proj1 {[x,y]}
proj2 {[x,y]} = {y}
thus
proj2 {[x,y]} c= {y}
XBOOLE_0:def 10 {y} c= proj2 {[x,y]}
thus
{y} c= proj2 {[x,y]}
verum