( {(prop 0)} |= prop 0 & not {(prop 0)} |=0 'G' (prop 0) ) by th21cp;
hence ex F being Subset of LTLB_WFF ex A being Element of LTLB_WFF st
( F |= A & not F |=0 'G' A ) ; :: thesis: verum