let X be set ; :: thesis: for R being Rule
for a being object holds
( X,R |- a iff for Y being X -extending b₁ -closed set holds a in Y )
let R be Rule; :: thesis: for a being object holds
( X,R |- a iff for Y being X -extending R -closed set holds a in Y )
let a be object ; :: thesis: ( X,R |- a iff for Y being X -extending R -closed set holds a in Y )
thus ( X,R |- a implies for Y being X -extending R -closed set holds a in Y ) :: thesis: ( ( for Y being X -extending R -closed set holds a in Y ) implies X,R |- a )

proof

assume A1: X,R |- a ; :: thesis: for Y being X -extending R -closed set holds a in Y
let Y be X -extending R -closed set ; :: thesis: a in Y
defpred S₁[ object ] means $1 in Y;
Y is X -extending ;
then A2: for b being object st b in X holds
S₁[b] ;
A3: for Z being set
for b being object st [Z,b] in R & ( for c being object st c in Z holds
S₁[c] ) holds
S₁[b]

proof

let Z be set ; :: thesis: for b being object st [Z,b] in R & ( for c being object st c in Z holds
S₁[c] ) holds
S₁[b]
let b be object ; :: thesis: ( [Z,b] in R & ( for c being object st c in Z holds
S₁[c] ) implies S₁[b] )
assume that
A5: [Z,b] in R and
A6: for c being object st c in Z holds
S₁[c] ; :: thesis: S₁[b]
Z c= Y by A6;
hence S₁[b] by A5, Def28; :: thesis: verum

end;

for b being object st X,R |- b holds
S₁[b] from PROOFS_1:sch 3(A2, A3);
hence a in Y by A1; :: thesis: verum

end;

assume for Y being X -extending R -closed set holds a in Y ; :: thesis: X,R |- a
then a in Theorems (X,R) ;
hence X,R |- a by Def30r; :: thesis: verum