set p = the Element of S;
( 0. ( 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 } ) ;
hence union { the carrier of (p `1) where p is Element of S : verum } is non empty set by TARSKI:def 4; :: thesis: verum