let n be Nat; :: thesis: card (2Set (Seg n)) = n choose 2
{ Y where Y is Subset of (Seg n) : card Y = 2 } = 2Set (Seg n) by SGRAPH1:def 2;
hence card (2Set (Seg n)) = (card (Seg n)) choose 2 by Th9
.= n choose 2 by FINSEQ_1:57 ;
:: thesis: verum