scheme :: WAYBEL19:sch 1
TopInd{ F₁() -> TopLattice, P₁[ set ] } :

for A being Subset of F₁() st A is open holds
P₁[A]

provided

A1: ex K being prebasis of F₁() st
for A being Subset of F₁() st A in K holds
P₁[A] and
A2: for F being Subset-Family of F₁() st ( for A being Subset of F₁() st A in F holds
P₁[A] ) holds
P₁[ union F] and
A3: for A1, A2 being Subset of F₁() st P₁[A1] & P₁[A2] holds
P₁[A1 /\ A2] and
A4: P₁[ [#] F₁()]