set y = init v;
reconsider y = init v as strict elementary LTLnode over v ;
A1: y is Element of LTLNodes v by Def30;
{y} c= LTLStates v
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {y} or x in LTLStates v )
assume x in {y} ; :: thesis: x in LTLStates v
then x = y by TARSKI:def 1;
hence x in LTLStates v by A1; :: thesis: verum
end;
hence {(init v)} is Element of bool (LTLStates v) ; :: thesis: verum