let A be Element of LTLB_WFF ; :: thesis: ( {} LTLB_WFF |=0 A implies {} LTLB_WFF |=0 'X' A )

assume Z1: {} LTLB_WFF |=0 A ; :: thesis: {} LTLB_WFF |=0 'X' A

A1: {A} |= A by LTLAXIO1:23;

for B being Element of LTLB_WFF st B in {A} holds

{} LTLB_WFF |=0 B by TARSKI:def 1, Z1;

hence {} LTLB_WFF |=0 'X' A by th265, A1, LTLAXIO1:25; :: thesis: verum

assume Z1: {} LTLB_WFF |=0 A ; :: thesis: {} LTLB_WFF |=0 'X' A

A1: {A} |= A by LTLAXIO1:23;

for B being Element of LTLB_WFF st B in {A} holds

{} LTLB_WFF |=0 B by TARSKI:def 1, Z1;

hence {} LTLB_WFF |=0 'X' A by th265, A1, LTLAXIO1:25; :: thesis: verum