len (canFS A) = card A by Th5;
hence not canFS A is empty ; :: thesis: verum