theorem Th71: :: MODELC_2:71

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