theorem Th18: :: PSCOMP_1:18

for r, s being Real holds proj1 " ].r,s.[ = { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) }