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