set S1 = { s where s is Subset of REAL : ex a, b being Real st ( a <= b & ( for x being realnumber holds ( x in s iff ( a < x & x <= b ) ) ) ) } ; A1:
{ s where s is Subset of REAL : ex a, b being Real st ( a <= b & ( for x being realnumber holds ( x in s iff ( a < x & x <= b ) ) ) ) } c= II
let y be object ; :: according to TARSKI:def 3:: thesis: ( not y in { s where s is Subset of REAL : ex a, b being Real st ( a <= b & ( for x being realnumber holds ( x in s iff ( a < x & x <= b ) ) ) ) } or y in II ) assume
y in { s where s is Subset of REAL : ex a, b being Real st ( a <= b & ( for x being realnumber holds ( x in s iff ( a < x & x <= b ) ) ) ) }
; :: thesis: y in II then consider s0 being Subset of REAL such that A2:
( y = s0 & ex a, b being Real st ( a <= b & ( for x being realnumber holds ( x in s0 iff ( a < x & x <= b ) ) ) ) )
; consider a0, b0 being Real such that A3:
( a0 <= b0 & ( for x being realnumber holds ( x in s0 iff ( a0 < x & x <= b0 ) ) ) )
byA2; A4:
s0 c=].a0,b0.]