let s2 be Real; :: thesis: { |[sb,tb]| where sb, tb is Real : s2 < sb } is Subset of (REAL 2)
{ |[sb,tb]| where sb, tb is Real : s2 < sb } c= REAL 2

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { |[sb,tb]| where sb, tb is Real : s2 < sb } or y in REAL 2 )
assume y in { |[sb,tb]| where sb, tb is Real : s2 < sb } ; :: thesis: y in REAL 2
then ex s7, t7 being Real st
( |[s7,t7]| = y & s2 < s7 ) ;
hence y in REAL 2 ; :: thesis: verum

end;

hence { |[sb,tb]| where sb, tb is Real : s2 < sb } is Subset of (REAL 2) ; :: thesis: verum