let T be non empty TopStruct ; 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; 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; 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
; 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
; ( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] )
c1 \/ c2 = c
hence
( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] )
by Def12; verum