let a, b be Real; :: thesis: ( a <= b implies for P being Subset of R^1 st P = [.a,b.] holds

Closed-Interval-TSpace (a,b) = R^1 | P )

assume A1: a <= b ; :: thesis: for P being Subset of R^1 st P = [.a,b.] holds

Closed-Interval-TSpace (a,b) = R^1 | P

let P be Subset of R^1; :: thesis: ( P = [.a,b.] implies Closed-Interval-TSpace (a,b) = R^1 | P )

assume P = [.a,b.] ; :: thesis: Closed-Interval-TSpace (a,b) = R^1 | P

then [#] (Closed-Interval-TSpace (a,b)) = P by A1, Th18;

hence Closed-Interval-TSpace (a,b) = R^1 | P by PRE_TOPC:def 5; :: thesis: verum

Closed-Interval-TSpace (a,b) = R^1 | P )

assume A1: a <= b ; :: thesis: for P being Subset of R^1 st P = [.a,b.] holds

Closed-Interval-TSpace (a,b) = R^1 | P

let P be Subset of R^1; :: thesis: ( P = [.a,b.] implies Closed-Interval-TSpace (a,b) = R^1 | P )

assume P = [.a,b.] ; :: thesis: Closed-Interval-TSpace (a,b) = R^1 | P

then [#] (Closed-Interval-TSpace (a,b)) = P by A1, Th18;

hence Closed-Interval-TSpace (a,b) = R^1 | P by PRE_TOPC:def 5; :: thesis: verum