defpred S₁[ Element of LTLB_WFF , Element of LTLB_WFF ] means ex p, q being Element of LTLB_WFF st
( X = p 'U' q & c₂ = untn (p,q) );
set c = { A where A is Element of LTLB_WFF : ex B being Element of LTLB_WFF st
( S₁[B,A] & B in X ) } ;
A1: untn X = { A where A is Element of LTLB_WFF : ex B being Element of LTLB_WFF st
( S₁[B,A] & B in X ) }

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { A where A is Element of LTLB_WFF : ex B being Element of LTLB_WFF st
( S₁[B,A] & B in X ) } c= untn X

let x be object ; :: thesis: ( x in untn X implies x in { A where A is Element of LTLB_WFF : ex B being Element of LTLB_WFF st
( S₁[B,A] & B in X ) } )
assume x in untn X ; :: thesis: x in { A where A is Element of LTLB_WFF : ex B being Element of LTLB_WFF st
( S₁[B,A] & B in X ) }
then ex A, B being Element of LTLB_WFF st
( x = untn (A,B) & A 'U' B in X ) ;
hence x in { A where A is Element of LTLB_WFF : ex B being Element of LTLB_WFF st
( S₁[B,A] & B in X ) } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Element of LTLB_WFF : ex B being Element of LTLB_WFF st
( S₁[B,A] & B in X ) } or x in untn X )
assume x in { A where A is Element of LTLB_WFF : ex B being Element of LTLB_WFF st
( S₁[B,A] & B in X ) } ; :: thesis: x in untn X
then ex A being Element of LTLB_WFF st
( x = A & ex B being Element of LTLB_WFF st
( S₁[B,A] & B in X ) ) ;
hence x in untn X ; :: thesis: verum

end;

A2: now :: thesis: for w, x, y being Element of LTLB_WFF st S₁[w,x] & S₁[w,y] holds
x = y

let w be Element of LTLB_WFF ; :: thesis: for x, y being Element of LTLB_WFF st S₁[w,x] & S₁[w,y] holds
x = y
let x, y be Element of LTLB_WFF ; :: thesis: ( S₁[w,x] & S₁[w,y] implies x = y )
assume that
A3: S₁[w,x] and
A4: S₁[w,y] ; :: thesis: x = y
consider p, q being Element of LTLB_WFF such that
A5: w = p 'U' q and
A6: x = untn (p,q) by A3;
consider A, B being Element of LTLB_WFF such that
A7: w = A 'U' B and
A8: y = untn (A,B) by A4;
p = A by A5, A7, HILBERT2:19;
hence x = y by A5, A7, HILBERT2:19, A6, A8; :: thesis: verum

end;

A9: X is finite ;
{ A where A is Element of LTLB_WFF : ex B being Element of LTLB_WFF st
( S₁[B,A] & B in X ) } is finite from FRAENKEL:sch 28(A9, A2);
hence untn X is finite by A1; :: thesis: verum