let r, s be Real; :: thesis: ( proj2 . |[r,s]| = s & proj1 . |[r,s]| = r )
thus proj2 . |[r,s]| = |[r,s]| `2 by Def6
.= s by EUCLID:52 ; :: thesis: proj1 . |[r,s]| = r
thus proj1 . |[r,s]| = |[r,s]| `1 by Def5
.= r by EUCLID:52 ; :: thesis: verum