let H1, H2 be LTL-formula; :: thesis: for r being Element of Inf_seq AtomicFamily holds
( r |= 'not' (H1 '&' H2) iff r |= ('not' H1) 'or' ('not' H2) )
let r be Element of Inf_seq AtomicFamily; :: thesis: ( r |= 'not' (H1 '&' H2) iff r |= ('not' H1) 'or' ('not' H2) )
( r |= 'not' (H1 '&' H2) iff r |/= H1 '&' H2 ) by Th64;
then ( r |= 'not' (H1 '&' H2) iff ( not r |= H1 or not r |= H2 ) ) by Th65;
then ( r |= 'not' (H1 '&' H2) iff ( r |= 'not' H1 or r |= 'not' H2 ) ) by Th64;
hence ( r |= 'not' (H1 '&' H2) iff r |= ('not' H1) 'or' ('not' H2) ) by Th66; :: thesis: verum