:: deftheorem Def42 defines P#5 FOMODEL4:def 42 :
for S being Language
for b₂ being Relation of (bool (S -sequents)),(S -sequents) holds
( b₂ = P#5 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule5 Seqts ) );