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} )

hereby :: thesis: ( M |= {A} implies M |= A )

assume A1: M |= A ; :: thesis: M |= {A}
thus M |= {A} :: thesis: verum

proof

let p be Element of LTLB_WFF ; :: according to LTLAXIO1:def 13 :: thesis: ( p in {A} implies M |= p )
assume p in {A} ; :: thesis: M |= p
hence M |= p by A1, TARSKI:def 1; :: thesis: verum

end;

end;

A2: A in {A} by TARSKI:def 1;
assume M |= {A} ; :: thesis: M |= A
hence M |= A by A2, Def14; :: thesis: verum