let H1, H2 be LTL-formula; :: thesis: for r being Element of Inf_seq AtomicFamily holds
( r |= H1 'or' H2 iff ( r |= H1 or r |= H2 ) )
let r be Element of Inf_seq AtomicFamily ; :: thesis: ( r |= H1 'or' H2 iff ( r |= H1 or r |= H2 ) )
( r |= H1 'or' H2 iff r |= Evaluate (H1 'or' H2),AtomicKai ) by Def65;
then ( r |= H1 'or' H2 iff r |= (Evaluate H1,AtomicKai ) 'or' (Evaluate H2,AtomicKai ) ) by Th7;
then ( r |= H1 'or' H2 iff ( r |= Evaluate H1,AtomicKai or r |= Evaluate H2,AtomicKai ) ) by Th16;
hence ( r |= H1 'or' H2 iff ( r |= H1 or r |= H2 ) ) by Def65; :: thesis: verum