theorem Th20: :: PSCOMP_1:20

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