theorem Th65: :: PROOFS_1:24

for X being set
for R being Rule
for a being object holds
( X,R |- a iff for Y being b₁ -extending b₂ -closed set holds a in Y )