theorem Th70: :: MODELC_2:70

for H1, H2 being LTL-formula
for r being Element of Inf_seq AtomicFamily holds
( r |= 'not' (H1 'or' H2) iff r |= ('not' H1) '&' ('not' H2) )