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