let H be LTL-formula; :: thesis: for r being Element of Inf_seq AtomicFamily st H is atomic holds
( r |= H iff H in (CastSeq r,AtomicFamily ) . 0 )
let r be Element of Inf_seq AtomicFamily ; :: thesis: ( H is atomic implies ( r |= H iff H in (CastSeq r,AtomicFamily ) . 0 ) )
assume A1: H is atomic ; :: thesis: ( r |= H iff H in (CastSeq r,AtomicFamily ) . 0 )
then A2: H in atomic_LTL ;
A3: ( r |= H iff r |= Evaluate H,AtomicKai ) by Def65;
ex f being Function of LTL_WFF ,the Assignations of (LTLModel AtomicFamily ,AtomicBasicAsgn ) st
( f is-Evaluation-for AtomicKai & Evaluate H,AtomicKai = f . H ) by Def33;
then Evaluate H,AtomicKai = AtomicKai . H by A1, Def27
.= AtomicAsgn H by A2, Def64 ;
then ( r |= H iff (Fid (AtomicAsgn H),(Inf_seq AtomicFamily )) . r = TRUE ) by A3, Def59;
then ( r |= H iff AtomicFunc H,r = TRUE ) by Def62;
hence ( r |= H iff H in (CastSeq r,AtomicFamily ) . 0 ) by Def61; :: thesis: verum