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

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