set Y = { r where r is Real : ( g < r & r < s ) } ;
let X be Subset of REAL; ( X = ].g,s.[ iff X = { r where r is Real : ( g < r & r < s ) } )
A1:
{ r where r is Real : ( g < r & r < s ) } c= ].g,s.[
].g,s.[ c= { r where r is Real : ( g < r & r < s ) }
hence
( X = ].g,s.[ iff X = { r where r is Real : ( g < r & r < s ) } )
by A1; verum