ex F being Subset of LTLB_WFF ex A being Element of LTLB_WFF st
( F |= A & not F |=0 'G' A )