theorem :: MODELC_2:36

for G, H being LTL-formula st G is_subformula_of H & H is_subformula_of G holds
G = H