:- op(200, xfy, inc).
:- op(200, xfy, egal_ens).
:- op(150,xfx,inter).
:- op(200, xfy, app).
definition(A inc B <=> ! [X]:(X app A => X app B)).
definition(parties(A) = [X , X inc A]).
definition(A inter B  =  [X , X app A  &  X app B]).
definition(egal_ens(A,B) <=> inc(A,B) & inc(B,A)).
% l'ensemble des parties d'une intersection est égale à l'intersection des parties
theoreme(ex2ter_thI21,![A,B] : (parties(A inter B) egal_ens parties(A) inter  parties(B))).
+++(app).