let r, s be real number ; :: thesis: proj1 " ].r,s.[ = { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) }
set Q = proj1 " ].r,s.[;
set QQ = { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) } ;

now

let z be set ; :: thesis: ( ( z in proj1 " ].r,s.[ implies z in { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) } ) & ( z in { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) } implies z in proj1 " ].r,s.[ ) )

hereby :: thesis: ( z in { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) } implies z in proj1 " ].r,s.[ )

assume A1: z in proj1 " ].r,s.[ ; :: thesis: z in { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) }
then reconsider p = z as Point of (TOP-REAL 2) ;
proj1 . p in ].r,s.[ by A1, FUNCT_2:46;
then consider t being Real such that
A2: ( t = proj1 . p & r < t & t < s ) ;
( p `1 = proj1 . p & p = |[(p `1 ),(p `2 )]| ) by Def28, EUCLID:57;
hence z in { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) } by A2; :: thesis: verum

end;

assume z in { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) } ; :: thesis: z in proj1 " ].r,s.[
then consider r1, r2 being Real such that
A3: ( z = |[r1,r2]| & r < r1 & r1 < s ) ;
set p = |[r1,r2]|;
A4: proj1 . |[r1,r2]| = |[r1,r2]| `1 by Def28
.= r1 by EUCLID:56 ;
r1 in ].r,s.[ by A3;
hence z in proj1 " ].r,s.[ by A3, A4, FUNCT_2:46; :: thesis: verum

end;

hence proj1 " ].r,s.[ = { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) } by TARSKI:2; :: thesis: verum