set T = bool (Subformulae v);
set Y = [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):];
defpred S₁[ object , object ] means ( $1 in [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):] & ex y1, y2, y3 being Subset of (Subformulae v) ex N being strict LTLnode over v st
( $1 = [[y1,y2],y3] & $2 = N & the LTLold of N = y1 & the LTLnew of N = y2 & the LTLnext of N = y3 ) );
A1: for x, y, z being object st S₁[x,y] & S₁[x,z] holds
y = z

proof

let x, y, z be object ; :: thesis: ( S₁[x,y] & S₁[x,z] implies y = z )
assume that
A2: S₁[x,y] and
A3: S₁[x,z] ; :: thesis: y = z
consider y1, y2, y3 being Subset of (Subformulae v), N1 being strict LTLnode over v such that
A4: x = [[y1,y2],y3] and
A5: ( y = N1 & the LTLold of N1 = y1 & the LTLnew of N1 = y2 & the LTLnext of N1 = y3 ) by A2;
consider z1, z2, z3 being Subset of (Subformulae v), N2 being strict LTLnode over v such that
A6: x = [[z1,z2],z3] and
A7: ( z = N2 & the LTLold of N2 = z1 & the LTLnew of N2 = z2 & the LTLnext of N2 = z3 ) by A3;
A8: y3 = z3 by A4, A6, XTUPLE_0:1;
A9: [y1,y2] = [z1,z2] by A4, A6, XTUPLE_0:1;
then y1 = z1 by XTUPLE_0:1;
hence y = z by A5, A7, A9, A8, XTUPLE_0:1; :: thesis: verum

end;

consider IT being set such that
A10: for x being object holds
( x in IT iff ex y being object st
( y in [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):] & S₁[y,x] ) ) from TARSKI:sch 1(A1);
not IT is empty

proof

set e = {} v;
set x = LTLnode(# ({} v),({} v),({} v) #);
set y = [[({} v),({} v)],({} v)];
[({} v),({} v)] in [:(bool (Subformulae v)),(bool (Subformulae v)):] by ZFMISC_1:def 2;
then [[({} v),({} v)],({} v)] in [:[:(bool (Subformulae v)),(bool (Subformulae v)):],(bool (Subformulae v)):] by ZFMISC_1:def 2;
then S₁[[[({} v),({} v)],({} v)], LTLnode(# ({} v),({} v),({} v) #)] by ZFMISC_1:def 3;
hence not IT is empty by A10; :: thesis: verum

end;

then reconsider IT = IT as non empty set ;
A11: for x being object st ex N being strict LTLnode over v st x = N holds
x in IT

proof

let x be object ; :: thesis: ( ex N being strict LTLnode over v st x = N implies x in IT )
assume ex N being strict LTLnode over v st x = N ; :: thesis: x in IT
then consider N being strict LTLnode over v such that
A12: x = N ;
set y3 = the LTLnext of N;
set y2 = the LTLnew of N;
set y1 = the LTLold of N;
set y = [[ the LTLold of N, the LTLnew of N], the LTLnext of N];
[ the LTLold of N, the LTLnew of N] in [:(bool (Subformulae v)),(bool (Subformulae v)):] by ZFMISC_1:def 2;
then [[ the LTLold of N, the LTLnew of N], the LTLnext of N] in [:[:(bool (Subformulae v)),(bool (Subformulae v)):],(bool (Subformulae v)):] by ZFMISC_1:def 2;
then [[ the LTLold of N, the LTLnew of N], the LTLnext of N] in [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):] by ZFMISC_1:def 3;
hence x in IT by A10, A12; :: thesis: verum

end;

take IT ; :: thesis: for x being object holds
( x in IT iff ex N being strict LTLnode over v st x = N )
for x being object st x in IT holds
ex N being strict LTLnode over v st x = N

proof

let x be object ; :: thesis: ( x in IT implies ex N being strict LTLnode over v st x = N )
assume x in IT ; :: thesis: ex N being strict LTLnode over v st x = N
then ex y being object st
( y in [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):] & S₁[y,x] ) by A10;
hence ex N being strict LTLnode over v st x = N ; :: thesis: verum

end;

hence for x being object holds
( x in IT iff ex N being strict LTLnode over v st x = N ) by A11; :: thesis: verum