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