assume not tau X is empty ; :: thesis: contradiction
then consider x being object such that
A1: x in tau X ;
ex p being Element of LTLB_WFF st
( p in X & x in tau1 . p ) by A1, Def5;
hence contradiction ; :: thesis: verum