1. The Irrationality of the Square Root of 2
IRRAT_1:1

  theorem :: IRRAT_1:1
   p is prime implies sqrt p is irrational;

2. Fundamental Theorem of Algebra
POLYNOM5:75

  theorem :: POLYNOM5:75
   for p be Polynomial of F_Complex st len p > 1 holds
    p is with_roots;

3. The Denumerability of the Rational Numbers
TOPGEN_3:17

  theorem :: TOPGEN_3:17
    Card RAT = alef 0;

4. Pythagorean Theorem
EUCLID_3:55

  theorem :: EUCLID_3:55
  for p1,p2,p3 st p1<>p2 & p3<>p2 &
      (angle(p1,p2,p3)=PI/2 or angle(p1,p2,p3)=3/2*PI) holds
      (|.p1-p2.|^2+|.p3-p2.|^2=|.p1-p3.|^2);

7. Law of Quadratic Reciprocity
INT_5:49

  theorem :: INT_5:49
  p>2 & q>2 & p<>q
    implies Lege(p,q)*Lege(q,p)=(-1)|^(((p-'1) div 2)*((q-'1) div 2));

10. Euler's Generalization of Fermat's Little Theorem
EULER_2:33

  theorem :: EULER_2:33 ::Euler's theorem
    a <> 0 & m > 1 & a,m are_relative_prime
                    implies (a |^ Euler m) mod m = 1;

11. The Infinitude of Primes
NEWTON:97

  theorem :: NEWTON:97 ::Euklidesa::
      SetPrimes is infinite;

13. Polyhedron Formula
POLYFORM:92

  theorem :: POLYFORM:92
  p is simply-connected & dim(p) = 3
    implies num-vertices(p) - num-edges(p) + num-faces(p) = 2;

15. Fundamental Theorem of Integral Calculus
INTEGRA5:13

  theorem :: INTEGRA5:13
  for f being PartFunc of REAL,REAL st A c= X & f is_differentiable_on X &
  f`|X is_integrable_on A & f`|X is_bounded_on A holds
  integral(f`|X,A) = f.(sup A)-f.(inf A);

17. De Moivre's Theorem
SIN_COS3:51

  theorem :: SIN_COS3:51
  for n being Nat, z being Element of COMPLEX holds
  (cos_C/.z + <i>*sin_C/.z) #N n = cos_C/.([*n,0*]*z) + <i>*sin_C/.([*n,0*]*z);

19. Four Squares Theorem
LAGRA4SQ:18

  theorem :: LAGRA4SQ:18
    for n be Nat holds
      ex x1,x2,x3,x4 be Nat st n = x1^2 + x2^2 + x3^2 + x4^2 ;

20. All Primes (1 mod 4) Equal the Sum of Two Squares
NAT_5:23

  theorem :: NAT_5:23
    p is prime & p mod 4 = 1 implies ex n,m st p = n^2 + m^2;

22. The Non-Denumerability of the Continuum
TOPGEN_3:30

  theorem :: TOPGEN_3:30
    alef 0 <` continuum;

23. Formula for Pythagorean Triples
PYTHTRIP:def 5

  definition
   redefine mode Pythagorean_triple means
  :: PYTHTRIP:def 5
    ex k,m,n st m <= n & it = { k*(n^2 - m^2), k*(2*m*n), k*(n^2 + m^2) };
  end;

25. Schroeder-Bernstein Theorem
KNASTER:12

  theorem :: KNASTER:12  :: Schroeder-Bernstein
   f is one-to-one & g is one-to-one implies
     ex h being Function of X,Y st h is bijective;

26. Leibniz's Series for Pi
LEIBNIZ1:14

  theorem :: LEIBNIZ1:14
    PI/4 = Sum Leibniz_Series;

27. Sum of the Angles of a Triangle
COMPLEX2:98

  theorem :: COMPLEX2:98
  a <> b & b <> c & 0 < angle(a,b,c) & angle(a,b,c) < PI
    implies angle(a,b,c)+angle(b,c,a)+angle(c,a,b) = PI &
            0 < angle(b,c,a) & 0 < angle(c,a,b);

30. The Ballot Problem
BALLOT_1:28

  theorem :: BALLOT_1:28
    A <> B & n >= k implies prob DominatedElection(A,n,B,k) = (n-k) / (n+k) ;

31. Ramsey's Theorem
RAMSEY_1:15

  theorem :: RAMSEY_1:15
    for X being infinite set,
        P being a_partition of the_subsets_of_card(n,X)
    st Card P = k holds
       ex H being Subset of X st H is infinite & H is_homogeneous_for P;

34. Divergence of the Harmonic Series
SERIES_1:37

  theorem :: SERIES_1:37
     p<=1 & (for n st n>=1 holds s.n=1/n to_power p) implies s is not summable;

35. Taylor's Theorem
TAYLOR_1:33

  theorem :: TAYLOR_1:33
   for n be Nat, f be PartFunc of REAL,REAL, x0,r be Real st
    ( 0 < r & f is_differentiable_on n+1, ].x0-r,x0+r.[ )
      for x be Real st x in ].x0-r, x0+r.[ holds
        ex s be Real st 0 < s & s < 1 &
          f.x=Partial_Sums(Taylor(f, ].x0-r,x0+r.[,x0,x)).n
                 + (diff(f,].x0-r,x0+r.[).(n+1)).(x0+s*(x-x0))
                 * (x-x0) |^ (n+1) / ((n+1)!);

36. Brouwer Fixed Point Theorem
BROUWER2:8

  theorem :: BROUWER2:8
    for A st A is compact non boundary
    for h be continuous Function of(TOP-REAL n) |A,(TOP-REAL n) |A
      holds h has_a_fixpoint;

37. The Solution of a Cubic
POLYEQ_5:15

  theorem :: POLYEQ_5:15
    q = (3*a1 - a2|^2)/9 & q <> 0 & r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 &
      s = 2-root(q|^3+r|^2) & s1 = 3-root(r+s) & s2 = -q/s1 implies
    ( z|^3+a2*z|^2+a1*z+a0 = 0
      iff
    z = s1+s2-a2/3 or
    z = -(s1+s2)/2-a2/3+(s1-s2)*(2-root 3)*<i>/2 or
    z = -(s1+s2)/2-a2/3-(s1-s2)*(2-root 3)*<i>/2);

38. Arithmetic Mean/Geometric Mean
RVSUM_3:47

  theorem :: RVSUM_3:47
    for f being non empty positive real-valued FinSequence holds
      GMean f <= Mean f ;

POLYEQ_5:16

  theorem :: POLYEQ_5:16
    q = (3*a1 - a2|^2)/9 & q = 0 & r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 &
    s1 = 3-root(2*r) implies
    ( z|^3+a2*z|^2+a1*z+a0 = 0 iff
    z = s1-a2/3 or
    z = -s1/2-a2/3+s1*(2-root 3)*<i>/2 or
    z = -s1/2-a2/3-s1*(2-root 3)*<i>/2);

42. Sum of the Reciprocals of the Triangular Numbers
NUMPOLY1:89

definition
  func ReciTriangRS -> Real_Sequence means
:: NUMPOLY1:def 13
    for i being Nat holds
      it.i = 1 / Triangle i;
end;
  theorem :: NUMPOLY1:89
    Sum ReciTriangRS = 2;

44. The Binomial Theorem
BINOM:26

  theorem :: BINOM:26
     for R being Abelian add-associative left_zeroed right_zeroed
              commutative associative add-cancelable
              distributive unital (non empty doubleLoopStr),
      a,b being Element of R,
      n being Nat
  holds (a+b)|^n = Sum((a,b) In_Power n);

45. The Partition Theorem

  theorem :: EULRPART:16
    card the set of all p where p is odd-valued a_partition of n
      =
    card the set of all p where p is one-to-one a_partition of n;

46. The Solution of the General Quartic Equation
POLYEQ_5:30

  definition
    let a0,a1,a2 be complex number;
    func 1_root_of_cubic(a0,a1,a2) -> complex number means
  :: POLYEQ_5:def 2
    ex r,s1 st r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s1 = 3-root(2*r) &
    it = s1-a2/3 if 3*a1 - a2|^2 = 0
    otherwise ex q,r,s,s1,s2 st q = (3*a1 - a2|^2)/9 &
    r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s = 2-root(q|^3+r|^2) &
    s1 = 3-root(r+s) & s2 = -q/s1 & it = s1+s2-a2/3;
    func 2_root_of_cubic(a0,a1,a2) -> complex number means
  :: POLYEQ_5:def 3
    ex r,s1 st r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s1 = 3-root(2*r) &
    it = -s1/2-a2/3+s1*(2-root 3)*<i>/2 if 3*a1 - a2|^2 = 0
    otherwise ex q,r,s,s1,s2 st q = (3*a1 - a2|^2)/9 &
    r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s = 2-root(q|^3+r|^2) &
    s1 = 3-root(r+s) & s2 = -q/s1 &
    it = -(s1+s2)/2-a2/3+(s1-s2)*(2-root 3)*<i>/2;
    func 3_root_of_cubic(a0,a1,a2) -> complex number means
  :: POLYEQ_5:def 4
    ex r,s1 st r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s1 = 3-root(2*r) &
    it = -s1/2-a2/3-s1*(2-root 3)*<i>/2 if 3*a1 - a2|^2 = 0
    otherwise ex q,r,s,s1,s2 st q = (3*a1 - a2|^2)/9 &
    r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s = 2-root(q|^3+r|^2) &
    s1 = 3-root(r+s) & s2 = -q/s1 &
    it = -(s1+s2)/2-a2/3-(s1-s2)*(2-root 3)*<i>/2;
  end;

  definition
    let a0,a1,a2,a3 be complex number;
    func 1_root_of_quartic(a0,a1,a2,a3) -> complex number means
  :: POLYEQ_5:def 5
    ex p,r,s1 st p = (8*a2-3*a3|^2)/32 &
    r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(p|^2-r) &
    it = 2-root(-2*(p-s1))-a3/4 if 8*a1 -4*a2*a3 + a3|^3 = 0
    otherwise ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 &
    q = (8*a1 -4*a2*a3 + a3|^3)/64 &
    r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 &
    s1 = 2-root(1_root_of_cubic(-q|^2,p|^2-r,2*p)) &
    s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)) & s3 = -q/(s1*s2) &
    it = s1+s2+s3-a3/4;
    func 2_root_of_quartic(a0,a1,a2,a3) -> complex number means
  :: POLYEQ_5:def 6
    ex p,r,s1 st p = (8*a2-3*a3|^2)/32 &
    r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(p|^2-r) &
    it = -2-root(-2*(p-s1))-a3/4 if 8*a1 -4*a2*a3 + a3|^3 = 0
    otherwise ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 &
    q = (8*a1 -4*a2*a3 + a3|^3)/64 &
    r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 &
    s1 = 2-root(1_root_of_cubic(-q|^2,p|^2-r,2*p)) &
    s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)) & s3 = -q/(s1*s2) &
    it = -s1-s2+s3-a3/4;
    func 3_root_of_quartic(a0,a1,a2,a3) -> complex number means
  :: POLYEQ_5:def 7
    ex p,r,s1 st p = (8*a2-3*a3|^2)/32 &
    r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(p|^2-r) &
    it = 2-root(-2*(p+s1))-a3/4 if 8*a1 -4*a2*a3 + a3|^3 = 0
    otherwise ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 &
    q = (8*a1 -4*a2*a3 + a3|^3)/64 &
    r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 &
    s1 = 2-root(1_root_of_cubic(-q|^2,p|^2-r,2*p)) &
    s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)) & s3 = -q/(s1*s2) &
    it = -s1+s2-s3-a3/4;
    func 4_root_of_quartic(a0,a1,a2,a3) -> complex number means
  :: POLYEQ_5:def 8
    ex p,r,s1 st p = (8*a2-3*a3|^2)/32 &
    r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(p|^2-r) &
    it = -2-root(-2*(p+s1))-a3/4 if 8*a1 -4*a2*a3 + a3|^3 = 0
    otherwise ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 &
    q = (8*a1 -4*a2*a3 + a3|^3)/64 &
    r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 &
    s1 = 2-root(1_root_of_cubic(-q|^2,p|^2-r,2*p)) &
    s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)) & s3 = -q/(s1*s2) &
    it = s1-s2-s3-a3/4;
  end;

  theorem :: POLYEQ_5:30
    a4 <> 0 implies (a4*z|^4 + a3*z|^3 + a2*z|^2 + a1*z + a0 = 0
      iff z = 1_root_of_quartic(a0/a4,a1/a4,a2/a4,a3/a4) or
          z = 2_root_of_quartic(a0/a4,a1/a4,a2/a4,a3/a4) or
          z = 3_root_of_quartic(a0/a4,a1/a4,a2/a4,a3/a4) or
          z = 4_root_of_quartic(a0/a4,a1/a4,a2/a4,a3/a4));

51. Wilson's Theorem
NAT_5:22

  theorem :: NAT_5:22
    n is prime iff (n-'1)! + 1 mod n = 0 & n>1;

52. The Number of Subsets of a Set
CARD_2:44

  theorem :: CARD_2:44
    exp(2,Card X) = Card bool X;

54. Konigsberg Bridges Problem
GRAPH_3A:5

  theorem :: GRAPH_3A:5
    not ex p being Path of KoenigsbergBridges st p is cyclic Eulerian ;

55. Product of Segments of Chords
EUCLID_6:38

  theorem :: EUCLID_6:38
    p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r) &
    p4 in circle(a,b,r) & p in LSeg(p1,p3) & p in LSeg(p2,p4) implies
    |.p1-p.|*|.p-p3.| = |.p2-p.|*|.p-p4.|;

57. Heron's Formula
EUCLID_6:39

  theorem :: EUCLID_6:39
    a = |.p2-p1.| & b = |.p3-p2.| & c = |.p1-p3.| &
      s = the_perimeter_of_polygon3(p1,p2,p3)/2 implies
    abs(the_area_of_polygon3(p1,p2,p3)) = sqrt(s*(s-a)*(s-b)*(s-c));

58. Formula for the Number of Combinations
CARD_FIN:18

  theorem :: CARD_FIN:18
    x<>y implies card Choose(X,k,x,y)=card X choose k;

60. Bezout's Theorem
NEWTON:81

  theorem :: NEWTON:81
   for m,n st m>0 or n>0 holds ex i,i1 st i*m + i1*n = m hcf n;

61. Theorem of Ceva
MENELAUS:21

  theorem :: MENELAUS:21
    (A, B, C is_a_triangle &
    A1 = (1 - lambda) * B + lambda * C &
    B1 = (1 - mu) * C + mu * A &
    C1 = (1 - nu) * A + nu * B &
    lambda <> 1 & mu <> 1 & nu <> 1 & ((1 - mu) + lambda * mu) <> 0 &
    ((1 - lambda) + nu * lambda) <> 0 & ((1 - nu) + mu * nu) <> 0) implies
    ((lambda / (1 - lambda)) * (mu / (1 - mu)) * (nu / (1 - nu)) = 1
      iff
    (ex A2 st A, A1, A2 is_collinear &
              B, B1, A2 is_collinear &
              C, C1, A2 is_collinear));

63. Cantor's Theorem
CARD_1:30

  theorem :: CARD_1:30
    Card X <` Card bool X;

64. L'Hôpital's Rule
L_HOSPIT:10

  theorem :: L_HOSPIT:10
     (ex N being Neighbourhood of x0 st f is_differentiable_on N &
  g is_differentiable_on N & N \ {x0} c= dom (f/g) &
  N c= dom ((f`|N)/(g`|N)) & f.x0 = 0 & g.x0 = 0 &
  (f`|N)/(g`|N) is_continuous_in x0)
  implies f/g is_convergent_in x0 & lim(f/g,x0) = diff(f,x0)/diff(g,x0);

65. Isosceles Triangle Theorem
EUCLID_6:19

  theorem :: EUCLID_6:16
    |.p3-p1.|=|.p2-p3.| & p1<>p2 implies angle(p3,p1,p2)=angle(p1,p2,p3);

66. Sum of a Geometric Series
SERIES_1:26

  theorem :: SERIES_1:26
  a <> 1 implies Partial_Sums(a GeoSeq).n = (1 - a to_power (n+1))/(1-a);

68. Sum of an arithmetic series
SERIES_2:42

  theorem :: SERIES_2:42
    (for n holds s.n = a*n+b) implies
      for n holds Partial_Sums(s).n = (n+1)*(s.0 + s.n)/2;

69. Greatest Common Divisor Algorithm
NAT_1:sch 8

  scheme :: NAT_1:sch 8
   Euklides { Q(Nat)->Nat, a,b()->Nat } :
    ex n st Q(n) = a() hcf b() & Q(n + 1) = 0
     provided
     0 < b() & b() < a() and
     Q(0) = a() & Q(1) = b() and
     for n holds Q(n + 2) = Q(n) mod Q(n + 1);

70. The Perfect Number Theorem
NAT_5:39

  theorem :: NAT_5:39
    n0 is even & n0 is perfect implies
    ex p being natural number
    st 2|^p -' 1 is prime & n0 = 2|^(p -' 1)*(2|^p -' 1);

71. Order of a Subgroup
GROUP_2:177

  theorem :: GROUP_2:177
   G is finite implies ord G = ord H * index H;

72. Sylow's Theorem
GROUP_10:12

  theorem :: GROUP_10:12
    for G being finite Group, p being prime (natural number)
    holds ex P being Subgroup of G st P is_Sylow_p-subgroup_of_prime p;

GROUP_10:14

  theorem :: GROUP_10:14
    for G being finite Group, p being prime (natural number) holds
      (for H being Subgroup of G st H is_p-group_of_prime p holds
        ex P being Subgroup of G st
        P is_Sylow_p-subgroup_of_prime p & H is Subgroup of P) &
      (for P1,P2 being Subgroup of G
        st P1 is_Sylow_p-subgroup_of_prime p & P2 is_Sylow_p-subgroup_of_prime p
        holds P1,P2 are_conjugated);

GROUP_10:15

  theorem :: GROUP_10:15
    for G being finite Group, p being prime (natural number) holds
      card the_sylow_p-subgroups_of_prime(p,G) mod p = 1 &
      card the_sylow_p-subgroups_of_prime(p,G) divides ord G;

73. Ascending or Descending Sequences
DILWORTH:56

  theorem :: DILWORTH:56
   for f being real-valued FinSequence, n being Nat
    st card f = n^2+1 & f is one-to-one
     ex g being real-valued FinSubsequence
      st g c= f & card g >= n+1 & (g is increasing or g is decreasing);

74. The Principle of Mathematical Induction
NAT_1:sch 1

  scheme :: NAT_1:sch 1
   Ind { P[Nat] } :
   for k being Nat holds P[k]
     provided
     P[0] and
     for k being Nat st P[k] holds P[k + 1];

75. The Mean Value Theorem
ROLLE:3

  theorem :: ROLLE:3
  for p,g st p<g for f st
  f is_continuous_on [.p,g.] & f is_differentiable_on ].p,g.[
  ex x0 st x0 in ].p,g.[ & diff(f,x0)=(f.g-f.p)/(g-p);

78. The Cauchy-Schwarz Inequality
HERMITAN:48

  theorem :: HERMITAN:48
  :: Schwarz inequality
  for V be VectSp of F_Complex, v,w be Vector of V
  for f be diagReR+0valued hermitan-Form of V
  holds |. f.[v,w] .|^2 <= signnorm(f,v) * signnorm(f,w);

79. The Intermediate Value Theorem
TOPREAL5:10

  theorem :: TOPREAL5:10 ::General Intermediate Value Point Theorem
         for X being non empty TopSpace,xa,xb being Point of X,
     a,b,d being Real,f being continuous map of X,R^1 st
     X is connected & f.xa=a & f.xb=b & a<=d & d<=b
     ex xc being Point of X st f.xc =d;

80. The Fundamental Theorem of Arithmetic
NAT_3:61

  theorem :: NAT_3:61
   Product ppf n = n;

INT_7:15

  theorem :: INT_7:15
    for p,q be bag of SetPrimes st p is prime-factorization-like &q
    is prime-factorization-like& Product p = Product q holds p=q;

83. The Friendship Theorem
FRIENDS1:14

  theorem :: FRIENDS1:14
    FSG is non empty implies FSG is with_universal_friend;

84. Morley's Theorem
EUCLID11:22

  theorem :: EUCLID11:22
    A,B,C is_a_triangle & angle(A,B,C) < PI &
    angle(E,C,A) = angle(B,C,A) / 3 &
    angle(C,A,E) = angle(C,A,B) / 3 &
    angle(A,B,F) = angle(A,B,C) / 3 &
    angle(F,A,B) = angle(C,A,B) / 3 &
    angle(B,C,G) = angle(B,C,A) / 3 &
    angle(G,B,C) = angle(A,B,C) / 3
    implies
    |.F-E.| = |.G-F.| & |.F-E.| = |.E-G.| & |.G-F.| = |.E-G.|;

85. Divisibility by 3 Rule
NUMERAL1:12

  theorem :: NUMERAL1:12
    for n being natural number holds
    3 divides n iff 3 divides Sum digits(n,10);

86. Lebesgue Measure and Integration
MESFUNC5:def 16

  definition
    let X be non empty set;
    let S be SigmaField of X;
    let M be sigma_Measure of S;
    let f be PartFunc of X,ExtREAL;
    func Integral(M,f) -> Element of ExtREAL equals
  :: MESFUNC5:def 16
    integral+(M,max+f)-integral+(M,max-f);
  end;

87. Desargues's Theorem
registration in ANPROJ_2

  registration let V be up-3-dimensional RealLinearSpace;
   cluster ProjectiveSpace V -> Fanoian Desarguesian Pappian;
  end;

88. Derangements Formula
CARDFIN2:10

  theorem :: CARDFIN2:10
    for s being non empty finite set
    holds card (derangements s) = round ((card s)! / number_e);

89. The Factor and Remainder Theorems
UPROOTS:52

  theorem :: UPROOTS:52  :: Factor theorem (Bezout)
    for L being non degenerated comRing, r being Element of L, p
  being Polynomial of L st r is_a_root_of p holds p = <%-r,1.L%>*'poly_quotient(p
    ,r);

91. The Triangle Inequality
EUCLID:16

  theorem :: EUCLID:16
  |.x1 - x2.| <= |.x1.| + |.x2.|;

93. The Birthday Problem
CARDFIN2:18

  theorem :: CARDFIN2:18
    for s, t being non empty finite set st card s = 23 & card t = 365
    holds prob (not-one-to-one (s, t)) > 1/2;

96. Principle of Inclusion/Exclusion
CARD_FIN:67

  theorem :: CARD_FIN:67
    for Fy be finite-yielding Function,X st dom Fy=X
      for XFS be XFinSequence of INT st
            dom XFS= card X &
            for n st n in dom XFS holds XFS.n=((-1)|^n)*Card_Intersection(Fy,n+1)
        holds
    Card union rng Fy=Sum XFS;

94. The Law of Cosines
EUCLID_6:7

  theorem :: EUCLID_6:7
    a = |.p1-p2.| & b = |.p3-p2.| & c = |.p3-p1.|
    implies c^2 = a^2 + b^2 - 2*a*b * cos angle(p1,p2,p3);

95. Ptolemy's Theorem
EUCLID_6:40

  theorem :: EUCLID_6:40
    p1 in circle(a,b,r) & p2 in circle(a,b,r) & p3 in circle(a,b,r) &
    p4 in circle(a,b,r) & p in LSeg(p1,p3) & p in LSeg(p2,p4) implies
    |.p3-p1.|*|.p4-p2.| = |.p2-p1.|*|.p4-p3.| + |.p3-p2.|*|.p4-p1.|;

96. Bertrand's Postulate
NAT_4:56

  theorem :: NAT_4:56
    for n being Element of NAT st n>=1 holds ex p being Prime st n<p & p<=2*n;

97. Cramer's Rule
LAPLACE:40

  theorem :: LAPLACE:40
    for A be Matrix of n,K st Det A <> 0.K
      for x,b be FinSequence of K st len x = n & x * A = <*b*> holds
        <*x*> = b * A~ &
        for i st i in Seg n holds
          x.i = (Det A)" * Det ReplaceLine(A,i,b);