deffunc H_{3}( Element of LTLB_WFF ) -> Element of bool LTLB_WFF = Sub . X;

A1: X is finite ;

{ H_{3}(A) where A is Element of LTLB_WFF : A in X } is finite
from FRAENKEL:sch 21(A1);

hence Subt X is finite ; :: thesis: Subt X is finite-membered

let x be set ; :: according to FINSET_1:def 6 :: thesis: ( not x in Subt X or x is finite )

assume x in Subt X ; :: thesis: x is finite

then ex A being Element of LTLB_WFF st

( x = Sub . A & A in X ) ;

hence x is finite ; :: thesis: verum

A1: X is finite ;

{ H

hence Subt X is finite ; :: thesis: Subt X is finite-membered

let x be set ; :: according to FINSET_1:def 6 :: thesis: ( not x in Subt X or x is finite )

assume x in Subt X ; :: thesis: x is finite

then ex A being Element of LTLB_WFF st

( x = Sub . A & A in X ) ;

hence x is finite ; :: thesis: verum