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

{} 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