let f, g be FinSequence of CQC-WFF ; :: thesis: ( Ant f is_Subsequence_of Ant g & Suc f = Suc g & Ant f |= Suc f implies Ant g |= Suc g )
assume A1: ( Ant f is_Subsequence_of Ant g & Suc f = Suc g & Ant f |= Suc f ) ; :: thesis: Ant g |= Suc g
let A be non empty set ; :: according to CALCUL_1:def 15 :: thesis: for J being interpretation of A
for v being Element of Valuations_in A st J,v |= Ant g holds
J,v |= Suc g
let J be interpretation of A; :: thesis: for v being Element of Valuations_in A st J,v |= Ant g holds
J,v |= Suc g
let v be Element of Valuations_in A; :: thesis: ( J,v |= Ant g implies J,v |= Suc g )
assume A2: J,v |= rng (Ant g) ; :: according to CALCUL_1:def 14 :: thesis: J,v |= Suc g

now

let p be Element of CQC-WFF ; :: thesis: ( p in rng (Ant f) implies J,v |= p )
assume A3: p in rng (Ant f) ; :: thesis: J,v |= p
rng (Ant f) c= rng (Ant g) by A1, Th1;
hence J,v |= p by A2, A3, Def11; :: thesis: verum

end;

then J,v |= rng (Ant f) by Def11;
then J,v |= Ant f by Def14;
hence J,v |= Suc g by A1, Def15; :: thesis: verum