scheme :: ARMSTRNG:sch 2
FinIntersect{ F₁() -> non empty finite set , P₁[ set ] } :

for x being set st x in F₁() holds
P₁[x]

provided

A1: for x being set st x is_/\-irreducible_in F₁() holds
P₁[x] and
A2: for x, y being set st x in F₁() & y in F₁() & P₁[x] & P₁[y] holds
P₁[x /\ y]