theorem :: SCPQSORT:13

for n, p0 being Nat holds card (QuickSort (n,p0)) = 57 by Lm28;