set p = the Element of S;
( 1. ( the Element of S `1) in the carrier of ( the Element of S `1) & the carrier of ( the Element of S `1) in { the carrier of (p `1) where p is Element of S : verum } ) ;
then reconsider e = 1. ( the Element of S `1) as Element of unionCarrier (S,f,E) by TARSKI:def 4;
take e ; :: thesis: ex p being Element of S st e = 1. (p `1)
thus ex p being Element of S st e = 1. (p `1) ; :: thesis: verum