(F ") .: W2 is (F ") " -defined ;
then (F ") .: W2 is F -defined by Th70;
hence (F ") .: W2 is F -defined Walk of G1 ; :: thesis: verum