set R = { [r,s] where r, s is Real : r <= s } ;
let x be set ; :: according to TARSKI:def 3,RELSET_1:def 1 :: thesis: ( not x in { [r,s] where r, s is Real : r <= s } or x in [:REAL ,REAL :] )
assume x in { [r,s] where r, s is Real : r <= s } ; :: thesis: x in [:REAL ,REAL :]
then ex r, s being Real st
( x = [r,s] & r <= s ) ;
hence x in [:REAL ,REAL :] by ZFMISC_1:106; :: thesis: verum