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

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

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

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

A in {A} by TARSKI:def 1;

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

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

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

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

A in {A} by TARSKI:def 1;

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