the Element of F " in F "" by Th21;
hence not F "" is empty ; :: thesis: verum