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 Def67;
then ( r |= H1 '&' H2 iff r |= (Evaluate (H1,AtomicKai)) '&' (Evaluate (H2,AtomicKai)) ) by Th51;
then ( r |= H1 '&' H2 iff ( r |= Evaluate (H1,AtomicKai) & r |= Evaluate (H2,AtomicKai) ) ) by Th58;
hence ( r |= H1 '&' H2 iff ( r |= H1 & r |= H2 ) ) by Def67; :: thesis: verum