let y be set ; :: thesis: for S being Language
for SQ being b₁ -sequents-like set
for R being Relation of (bool (S -sequents)),(S -sequents) holds
( y in (FuncRule R) . SQ iff ( y in S -sequents & [SQ,y] in R ) )
let S be Language; :: thesis: for SQ being S -sequents-like set
for R being Relation of (bool (S -sequents)),(S -sequents) holds
( y in (FuncRule R) . SQ iff ( y in S -sequents & [SQ,y] in R ) )
let SQ be S -sequents-like set ; :: thesis: for R being Relation of (bool (S -sequents)),(S -sequents) holds
( y in (FuncRule R) . SQ iff ( y in S -sequents & [SQ,y] in R ) )
set Q = S -sequents ;
let R be Relation of (bool (S -sequents)),(S -sequents); :: thesis: ( y in (FuncRule R) . SQ iff ( y in S -sequents & [SQ,y] in R ) )
reconsider F = FuncRule R as Function of (bool (S -sequents)),(bool (S -sequents)) ;
reconsider Seqts = SQ as Element of bool (S -sequents) by DefSeqtLike2;
set G = { x where x is Element of S -sequents : [Seqts,x] in R } ;
B2: F . Seqts = { x where x is Element of S -sequents : [Seqts,x] in R } by DefFr;
B3: F . Seqts c= S -sequents ;
thus ( y in (FuncRule R) . SQ implies ( y in S -sequents & [SQ,y] in R ) ) :: thesis: ( y in S -sequents & [SQ,y] in R implies y in (FuncRule R) . SQ )

proof

assume CC0: y in (FuncRule R) . SQ ; :: thesis: ( y in S -sequents & [SQ,y] in R )
thus y in S -sequents by B3, CC0; :: thesis: [SQ,y] in R
consider x being Element of S -sequents such that
C1: ( y = x & [Seqts,x] in R ) by CC0, B2;
thus [SQ,y] in R by C1; :: thesis: verum

end;

assume B4: ( y in S -sequents & [SQ,y] in R ) ; :: thesis: y in (FuncRule R) . SQ
then reconsider seqt = y as Element of S -sequents ;
seqt in F . Seqts by Lm1, B4;
hence y in (FuncRule R) . SQ ; :: thesis: verum