let r, s be Real; :: thesis: proj2 " ].r,s.[ = { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) }
set Q = proj2 " ].r,s.[;
set QQ = { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) } ;
now :: thesis: for z being object holds
( ( z in proj2 " ].r,s.[ implies z in { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) } ) & ( z in { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) } implies z in proj2 " ].r,s.[ ) )
let z be object ; :: thesis: ( ( z in proj2 " ].r,s.[ implies z in { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) } ) & ( z in { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) } implies z in proj2 " ].r,s.[ ) )
hereby :: thesis: ( z in { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) } implies z in proj2 " ].r,s.[ )
assume A1: z in proj2 " ].r,s.[ ; :: thesis: z in { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) }
then reconsider p = z as Point of (TOP-REAL 2) ;
proj2 . p in ].r,s.[ by A1, FUNCT_2:38;
then A2: ex t being Real st
( t = proj2 . p & r < t & t < s ) ;
( p `2 = proj2 . p & p = |[(p `1),(p `2)]| ) by Def6, EUCLID:53;
hence z in { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) } by A2; :: thesis: verum
end;
assume z in { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) } ; :: thesis: z in proj2 " ].r,s.[
then consider r1, r2 being Real such that
A3: z = |[r1,r2]| and
A4: ( r < r2 & r2 < s ) ;
set p = |[r1,r2]|;
A5: r2 in ].r,s.[ by A4;
proj2 . |[r1,r2]| = |[r1,r2]| `2 by Def6
.= r2 by EUCLID:52 ;
hence z in proj2 " ].r,s.[ by A3, A5, FUNCT_2:38; :: thesis: verum
end;
hence proj2 " ].r,s.[ = { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) } by TARSKI:2; :: thesis: verum