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 Def3;
set G = { x where x is Element of S -sequents : [Seqts,x] in R } ;
A1: F . Seqts = { x where x is Element of S -sequents : [Seqts,x] in R } by Def47;
A2: 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 A3: y in (FuncRule R) . SQ ; :: thesis: ( y in S -sequents & [SQ,y] in R )
thus y in S -sequents by A2, A3; :: thesis: [SQ,y] in R
consider x being Element of S -sequents such that
A4: ( y = x & [Seqts,x] in R ) by A3, A1;
thus [SQ,y] in R by A4; :: thesis: verum

end;

assume A5: ( 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 Lm27, A5;
hence y in (FuncRule R) . SQ ; :: thesis: verum