let H be ZF-formula; :: thesis: H is_subformula_of H
take 1 ; :: according to ZF_LANG:def 40 :: thesis: ex L being FinSequence st
( 1 <= 1 & len L = 1 & L . 1 = H & L . 1 = H & ( for k being Element of NAT st 1 <= k & k < 1 holds
ex H1, F1 being ZF-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
take <*H*> ; :: thesis: ( 1 <= 1 & len <*H*> = 1 & <*H*> . 1 = H & <*H*> . 1 = H & ( for k being Element of NAT st 1 <= k & k < 1 holds
ex H1, F1 being ZF-formula st
( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus 1 <= 1 ; :: thesis: ( len <*H*> = 1 & <*H*> . 1 = H & <*H*> . 1 = H & ( for k being Element of NAT st 1 <= k & k < 1 holds
ex H1, F1 being ZF-formula st
( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus len <*H*> = 1 by FINSEQ_1:40; :: thesis: ( <*H*> . 1 = H & <*H*> . 1 = H & ( for k being Element of NAT st 1 <= k & k < 1 holds
ex H1, F1 being ZF-formula st
( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus ( <*H*> . 1 = H & <*H*> . 1 = H ) ; :: thesis: for k being Element of NAT st 1 <= k & k < 1 holds
ex H1, F1 being ZF-formula st
( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 )
thus for k being Element of NAT st 1 <= k & k < 1 holds
ex H1, F1 being ZF-formula st
( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ; :: thesis: verum