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 )
consider f being Function of LTL_WFF ,the Assignations of (LTLModel AtomicFamily ,AtomicBasicAsgn ) such that
A2: ( f is-Evaluation-for AtomicKai & Evaluate H,AtomicKai = f . H ) by Def32;
A3: H in atomic_LTL by A1;
A4: Evaluate H,AtomicKai = AtomicKai . H by A1, A2, Def26
.= AtomicAsgn H by Def64, A3 ;
( r |= H iff r |= Evaluate H,AtomicKai ) by Def65;
then ( r |= H iff (Fid (AtomicAsgn H),(Inf_seq AtomicFamily )) . r = TRUE ) by A4, 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