let A be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F |= A & ( for B being Element of LTLB_WFF st B in F holds
{} LTLB_WFF |=0 B ) holds
{} LTLB_WFF |=0 A
let F be Subset of LTLB_WFF; :: thesis: ( F |= A & ( for B being Element of LTLB_WFF st B in F holds
{} LTLB_WFF |=0 B ) implies {} LTLB_WFF |=0 A )
assume Z1: ( F |= A & ( for B being Element of LTLB_WFF st B in F holds
{} LTLB_WFF |=0 B ) ) ; :: thesis: {} LTLB_WFF |=0 A
then for B being Element of LTLB_WFF st B in F holds
{} LTLB_WFF |= B by th262b, th264p;
hence {} LTLB_WFF |=0 A by th262b, th264p, th218, Z1; :: thesis: verum