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