set PCS = PRIM:CompSeq G;
(PRIM:CompSeq G) .Result() = (PRIM:CompSeq G) . ((PRIM:CompSeq G) .Lifespan()) ;
hence (PRIM:CompSeq G) .Result() is PRIM:Labeling of G ; :: thesis: verum