let A be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st A in LTL0_axioms holds
F |=0 A
let F be Subset of LTLB_WFF; :: thesis: ( A in LTL0_axioms implies F |=0 A )
assume A in LTL0_axioms ; :: thesis: F |=0 A
then consider B being Element of LTLB_WFF such that
A8: ( A = 'G' B & B in LTL_axioms ) ;
{} LTLB_WFF |- B by LTLAXIO1:42, A8;
then {} LTLB_WFF |= 'G' B by LTLAXIO1:41, LTLAXIO1:54;
then B1: {} LTLB_WFF |=0 'G' B by th262b, th264p;
let M be LTLModel; :: according to LTLAXIO5:def 3 :: thesis: ( M |=0 F implies M |=0 A )
assume M |=0 F ; :: thesis: M |=0 A
M |=0 {} LTLB_WFF ;
hence M |=0 A by B1, A8; :: thesis: verum