let r, s be Real; 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 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 ;
( ( 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.[ ) )assume
z in { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) }
;
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;
verum end;
hence
proj1 " ].r,s.[ = { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) }
by TARSKI:2; verum