set DCS = DIJK:CompSeq src;
(DIJK:CompSeq src) .Result() = (DIJK:CompSeq src) . ((DIJK:CompSeq src) .Lifespan()) ;
hence (DIJK:CompSeq src) .Result() is DIJK:Labeling of G ; :: thesis: verum