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