let F be Subset of LTLB_WFF; :: thesis: for M being LTLModel st M |= F holds
M |=0 F
let M be LTLModel; :: thesis: ( M |= F implies M |=0 F )
assume Z1: M |= F ; :: thesis: M |=0 F
let A be Element of LTLB_WFF ; :: according to LTLAXIO5:def 2 :: thesis: ( A in F implies M |=0 A )
assume A in F ; :: thesis: M |=0 A
then M |= A by Z1;
hence M |=0 A ; :: thesis: verum