let T be non empty TopStruct ; :: thesis: for c being with_endpoints Curve of T
for r being Real ex c1, c2 being Element of Curves T st
( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] )

let c be with_endpoints Curve of T; :: thesis: for r being Real ex c1, c2 being Element of Curves T st
( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] )

let r be Real; :: thesis: ex c1, c2 being Element of Curves T st
( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] )

set c1 = c | [.(inf (dom c)),r.];
set c2 = c | [.r,(sup (dom c)).];
reconsider c1 = c | [.(inf (dom c)),r.] as Curve of T by Th26;
reconsider c2 = c | [.r,(sup (dom c)).] as Curve of T by Th26;
take c1 ; :: thesis: ex c2 being Element of Curves T st
( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] )

take c2 ; :: thesis: ( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] )
c1 \/ c2 = c
proof
per cases ( r < inf (dom c) or r >= inf (dom c) ) ;
suppose A1: r < inf (dom c) ; :: thesis: c1 \/ c2 = c
then [.(inf (dom c)),r.] = {} by XXREAL_1:29;
then A2: c1 = {} ;
[.(inf (dom c)),(sup (dom c)).] c= [.r,(sup (dom c)).] by ;
then dom c c= [.r,(sup (dom c)).] by Th27;
hence c1 \/ c2 = c by ; :: thesis: verum
end;
suppose A3: r >= inf (dom c) ; :: thesis: c1 \/ c2 = c
per cases ( r > sup (dom c) or r <= sup (dom c) ) ;
suppose A4: r > sup (dom c) ; :: thesis: c1 \/ c2 = c
then [.r,(sup (dom c)).] = {} by XXREAL_1:29;
then A5: c2 = {} ;
[.(inf (dom c)),(sup (dom c)).] c= [.(inf (dom c)),r.] by ;
then dom c c= [.(inf (dom c)),r.] by Th27;
hence c1 \/ c2 = c by ; :: thesis: verum
end;
suppose A6: r <= sup (dom c) ; :: thesis: c1 \/ c2 = c
dom c = [.(inf (dom c)),(sup (dom c)).] by Th27
.= [.(inf (dom c)),r.] \/ [.r,(sup (dom c)).] by ;
then c | (dom c) = c1 \/ c2 by RELAT_1:78;
hence c1 \/ c2 = c ; :: thesis: verum
end;
end;
end;
end;
end;
hence ( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] ) by Def12; :: thesis: verum