let r, s be Real; :: 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 :: thesis: for z being object holds
( ( 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.[ ) )

let z be object ; :: 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:38;
then A2: ex t being Real st
( t = proj1 . p & r < t & t < s ) ;
( p `1 = proj1 . p & p = |[(p `1),(p `2)]| ) by Def5, EUCLID:53;
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]| and
A4: ( r < r1 & r1 < s ) ;
set p = |[r1,r2]|;
A5: r1 in ].r,s.[ by A4;
proj1 . |[r1,r2]| = |[r1,r2]| `1 by Def5
.= r1 by EUCLID:52 ;
hence z in proj1 " ].r,s.[ by A3, A5, FUNCT_2:38; :: thesis: verum

end;

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