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 Th19;
then ( r |= 'not' (H1 'or' H2) iff ( not r |= H1 & not r |= H2 ) ) by Th21;
then ( r |= 'not' (H1 'or' H2) iff ( r |= 'not' H1 & r |= 'not' H2 ) ) by Th19;
hence ( r |= 'not' (H1 'or' H2) iff r |= ('not' H1) '&' ('not' H2) ) by Th20; :: thesis: verum