theorem Th11: :: LTLAXIO2:11

for A being Element of LTLB_WFF holds (con <*A*>) /. (len (con <*A*>)) = A