let A be Element of LTLB_WFF ; :: thesis: for M being LTLModel holds

( M |= A iff M |= {A} )

let M be LTLModel; :: thesis: ( M |= A iff M |= {A} )

thus ( M |= A implies M |= {A} ) by TARSKI:def 1; :: thesis: ( M |= {A} implies M |= A )

A in {A} by TARSKI:def 1;

hence ( M |= {A} implies M |= A ) ; :: thesis: verum

( M |= A iff M |= {A} )

let M be LTLModel; :: thesis: ( M |= A iff M |= {A} )

thus ( M |= A implies M |= {A} ) by TARSKI:def 1; :: thesis: ( M |= {A} implies M |= A )

A in {A} by TARSKI:def 1;

hence ( M |= {A} implies M |= A ) ; :: thesis: verum