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