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

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