theorem Th3: :: FOMODEL4:3

for S being Language
for SQ being b₁ -sequents-like set
for Sq being b₁ -sequent-like object
for R being Relation of (bool (S -sequents)),(S -sequents) st [SQ,Sq] in R holds
Sq in (FuncRule R) . SQ