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) ) ;
ex f being Function of LTL_WFF, the carrier of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn)) st
( f is-Evaluation-for AtomicKai & Evaluate (H,AtomicKai) = f . H ) by Def35;
then Evaluate (H,AtomicKai) = AtomicKai . H by A1
.= AtomicAsgn H by A2, Def62 ;
then ( r |= H iff (Fid ((AtomicAsgn H),(Inf_seq AtomicFamily))) . r = TRUE ) by A3;
then ( r |= H iff AtomicFunc (H,r) = TRUE ) by Def60;
hence ( r |= H iff H in (CastSeq (r,AtomicFamily)) . 0 ) by Def59; :: thesis: verum