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