theorem :: PSCOMP_1:65

for r, s being Real holds
( proj2 . |[r,s]| = s & proj1 . |[r,s]| = r )