%%%%%%%%%%%%%%%%%
%   theoremes   %
%%%%%%%%%%%%%%%%%

th1.
'transitivite de l inclusion dans l ensemble des parties'.
qqs(E,transitive(inc,parties(E))).
th2.
'parties(a inter b) = parties(a) inter parties(b)'. 
qqs(A, qqs(B, parties(A inter B) egal_ens parties(A) inter parties(B))).
th3.
'f(a union b) = f(a) union f(b)'.
qqs(X, qqs(Y, qqs(F, application(F, X, Y) => 
         qqs(A, qqs(B, image(F, A union B) egal_ens image(F,A) union image(F,B)
                    )
             )
                 )
          )
    ) .
th4.
'appartenir au meme element d une partition est une relation d equivalence'.
qqs(A, qqs(E, partition(A, E) => (qqs(R, qqs(X app E, qqs(Y app E, ..[R,X,Y] <=>
                                           ilexiste(Z app A, X app Z et Y app Z)
                                                          )
                                             )
                                         => equiv(E,R)
                                     )
                                  )
           )
    ) .