let s1 be Real; :: thesis: { |[tb,sb]| where tb, sb is Real : sb > s1 } is Subset of (TOP-REAL 2)

{ |[tb,sb]| where tb, sb is Real : sb > s1 } c= REAL 2

{ |[tb,sb]| where tb, sb is Real : sb > s1 } c= REAL 2

proof

hence
{ |[tb,sb]| where tb, sb is Real : sb > s1 } is Subset of (TOP-REAL 2)
by EUCLID:22; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { |[tb,sb]| where tb, sb is Real : sb > s1 } or y in REAL 2 )

assume y in { |[tb,sb]| where tb, sb is Real : sb > s1 } ; :: thesis: y in REAL 2

then ex t7, s7 being Real st

( |[t7,s7]| = y & s7 > s1 ) ;

hence y in REAL 2 by Lm2; :: thesis: verum

end;assume y in { |[tb,sb]| where tb, sb is Real : sb > s1 } ; :: thesis: y in REAL 2

then ex t7, s7 being Real st

( |[t7,s7]| = y & s7 > s1 ) ;

hence y in REAL 2 by Lm2; :: thesis: verum