let p be Element of PL-WFF ; :: thesis: for F, G being Subset of PL-WFF st F c= G & F |- p holds
G |- p
let F, G be Subset of PL-WFF; :: thesis: ( F c= G & F |- p implies G |- p )
assume Z0: F c= G ; :: thesis: ( not F |- p or G |- p )
assume F |- p ; :: thesis: G |- p
then consider f being FinSequence of PL-WFF such that
C1: ( f . (len f) = p & 1 <= len f & ( for k being Nat st 1 <= k & k <= len f holds
prc f,F,k ) ) ;
C17: len f in dom f by C1, FINSEQ_3:25;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len f implies G |- f /. $1 );

C2: now :: thesis: for s being Nat st ( for n being Nat st n < s holds
S₁[n] ) holds
S₁[s]

let s be Nat; :: thesis: ( ( for n being Nat st n < s holds
S₁[n] ) implies S₁[b₁] )
assume C5: for n being Nat st n < s holds
S₁[n] ; :: thesis: S₁[b₁]

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

suppose s = 0 ; :: thesis: S₁[b₁]

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

end;

suppose not s < 1 ; :: thesis: ( 1 <= b₁ & b₁ <= len f implies G |- f /. b₁ )

assume C7: ( 1 <= s & s <= len f ) ; :: thesis: G |- f /. s
then C3: prc f,F,s by C1;
C16: s in dom f by C7, FINSEQ_3:25;
thus G |- f /. s :: thesis: verum

proof

per cases ( f . s in PL_axioms or f . s in F or ex j, k being Nat st
( 1 <= j & j < s & 1 <= k & k < s & f /. j,f /. k MP_rule f /. s ) ) by C3;

suppose f . s in PL_axioms ; :: thesis: G |- f /. s

then f /. s in PL_axioms by C16, PARTFUN1:def 6;
hence G |- f /. s by th42; :: thesis: verum

end;

suppose f . s in F ; :: thesis: G |- f /. s

then f /. s in F by C16, PARTFUN1:def 6;
hence G |- f /. s by th42, Z0; :: thesis: verum

end;

suppose ex j, k being Nat st
( 1 <= j & j < s & 1 <= k & k < s & f /. j,f /. k MP_rule f /. s ) ; :: thesis: G |- f /. s

then consider j, k being Nat such that
C4: ( 1 <= j & j < s & 1 <= k & k < s & f /. j,f /. k MP_rule f /. s ) ;
C6: S₁[j] by C5, C4;
S₁[k] by C4, C5;
hence G |- f /. s by th43, C7, XXREAL_0:2, C4, C6; :: thesis: verum

end;

end;

end;

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 4(C2);
then G |- f /. (len f) by C1;
hence G |- p by C1, C17, PARTFUN1:def 6; :: thesis: verum