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

now :: thesis: for B being Element of LTLB_WFF st B in F holds
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;

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