let a, b be real number ; :: 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 & [#] (R^1 | P) = P ) by A1, Th25, PRE_TOPC:def 10;
hence Closed-Interval-TSpace a,b = R^1 | P by PRE_TOPC:def 10; :: thesis: verum