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 |= B ) holds

{} LTLB_WFF |= 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 |= B ) implies {} LTLB_WFF |= A )

assume Z1: ( F |= A & ( for B being Element of LTLB_WFF st B in F holds

{} LTLB_WFF |= B ) ) ; :: thesis: {} LTLB_WFF |= A

let M be LTLModel; :: according to LTLAXIO1:def 14 :: thesis: ( not M |= {} LTLB_WFF or M |= A )

assume Z2: M |= {} LTLB_WFF ; :: thesis: M |= A

hence M |= A by Z1; :: thesis: verum

{} LTLB_WFF |= B ) holds

{} LTLB_WFF |= 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 |= B ) implies {} LTLB_WFF |= A )

assume Z1: ( F |= A & ( for B being Element of LTLB_WFF st B in F holds

{} LTLB_WFF |= B ) ) ; :: thesis: {} LTLB_WFF |= A

let M be LTLModel; :: according to LTLAXIO1:def 14 :: thesis: ( not M |= {} LTLB_WFF or M |= A )

assume Z2: M |= {} LTLB_WFF ; :: thesis: M |= A

now :: thesis: for B being Element of LTLB_WFF st B in F holds

M |= B

then
M |= F
;M |= B

let B be Element of LTLB_WFF ; :: thesis: ( B in F implies M |= B )

assume B in F ; :: thesis: M |= B

then {} LTLB_WFF |= B by Z1;

hence M |= B by Z2; :: thesis: verum

end;assume B in F ; :: thesis: M |= B

then {} LTLB_WFF |= B by Z1;

hence M |= B by Z2; :: thesis: verum

hence M |= A by Z1; :: thesis: verum