let A, B be Element of PL-WFF ; :: thesis: for F being Subset of PL-WFF st F \/ {A} |- B holds
F |- A => B
let F be Subset of PL-WFF; :: thesis: ( F \/ {A} |- B implies F |- A => B )
assume F \/ {A} |- B ; :: thesis: F |- A => B
then consider f being FinSequence of PL-WFF such that
A1: f . (len f) = B and
A2: 1 <= len f and
A3: for i being Nat st 1 <= i & i <= len f holds
prc f,F \/ {A},i ;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len f implies F |- A => (f /. $1) );
A4: for i being Nat st ( for j being Nat st j < i holds
S₁[j] ) holds
S₁[i]

proof

let i be Nat; :: thesis: ( ( for j being Nat st j < i holds
S₁[j] ) implies S₁[i] )
assume A5: for j being Nat st j < i holds
S₁[j] ; :: thesis: S₁[i]

per cases ( i = 0 or not i < 1 ) by NAT_1:14;

suppose i = 0 ; :: thesis: S₁[i]

hence S₁[i] ; :: thesis: verum

end;

suppose not i < 1 ; :: thesis: S₁[i]

assume that
A6: 1 <= i and
A7: i <= len f ; :: thesis: F |- A => (f /. i)

per cases ( f . i in PL_axioms or f . i in F \/ {A} or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & f /. j,f /. k MP_rule f /. i ) ) by A3, A6, A7, defprc;

suppose A8: f . i in PL_axioms ; :: thesis: F |- A => (f /. i)

(f /. i) => (A => (f /. i)) in PL_axioms by withplax;
then A9: F |- (f /. i) => (A => (f /. i)) by th42;
f /. i in PL_axioms by A6, A7, A8, LTLAXIO5:1;
then F |- f /. i by th42;
hence F |- A => (f /. i) by th43, A9; :: thesis: verum

end;

suppose A10: f . i in F \/ {A} ; :: thesis: F |- A => (f /. i)

per cases ( f . i in F or f . i in {A} ) by A10, XBOOLE_0:def 3;

suppose A11: f . i in F ; :: thesis: F |- A => (f /. i)

(f /. i) => (A => (f /. i)) in PL_axioms by withplax;
then A12: F |- (f /. i) => (A => (f /. i)) by th42;
f /. i in F by A6, A7, A11, LTLAXIO5:1;
then F |- f /. i by th42;
hence F |- A => (f /. i) by th43, A12; :: thesis: verum

end;

suppose f . i in {A} ; :: thesis: F |- A => (f /. i)

then f . i = A by TARSKI:def 1;
then f /. i = A by A6, A7, LTLAXIO5:1;
hence F |- A => (f /. i) by thaa; :: thesis: verum

end;

end;

end;

suppose ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & f /. j,f /. k MP_rule f /. i ) ; :: thesis: F |- A => (f /. i)

then consider j, k being Nat such that
A15: 1 <= j and
A16: j < i and
A17: 1 <= k and
A18: k < i and
A19: f /. j,f /. k MP_rule f /. i ;
j <= len f by A7, A16, XXREAL_0:2;
then A20: F |- A => (f /. j) by A5, A15, A16;
k <= len f by A7, A18, XXREAL_0:2;
then A21: F |- A => (f /. k) by A5, A17, A18;
(A => ((f /. j) => (f /. i))) => ((A => (f /. j)) => (A => (f /. i))) in PL_axioms by withplax;
then A23: F |- (A => ((f /. j) => (f /. i))) => ((A => (f /. j)) => (A => (f /. i))) by th42;
F |- (A => (f /. j)) => (A => (f /. i)) by A23, th43, A21, A19;
hence F |- A => (f /. i) by A20, th43; :: thesis: verum

end;

end;

end;

end;

end;

A37: for i being Nat holds S₁[i] from NAT_1:sch 4(A4);
B = f /. (len f) by A1, A2, LTLAXIO5:1;
hence F |- A => B by A2, A37; :: thesis: verum