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,AtomicKai)) 'or' (Evaluate (H2,AtomicKai)) ) by Th52;
then ( r |= H1 'or' H2 iff ( r |= Evaluate (H1,AtomicKai) or r |= Evaluate (H2,AtomicKai) ) ) by Th61;
hence ( r |= H1 'or' H2 iff ( r |= H1 or r |= H2 ) ) ; :: thesis: verum