let f be FinSequence of CQC-WFF ; :: thesis: Ant (f ^ <*VERUM*>) |= Suc (f ^ <*VERUM*>)
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 (f ^ <*VERUM*>) holds
J,v |= Suc (f ^ <*VERUM*>)
let J be interpretation of A; :: thesis: for v being Element of Valuations_in A st J,v |= Ant (f ^ <*VERUM*>) holds
J,v |= Suc (f ^ <*VERUM*>)
let v be Element of Valuations_in A; :: thesis: ( J,v |= Ant (f ^ <*VERUM*>) implies J,v |= Suc (f ^ <*VERUM*>) )
assume J,v |= Ant (f ^ <*VERUM*>) ; :: thesis: J,v |= Suc (f ^ <*VERUM*>)
Suc (f ^ <*VERUM*>) = VERUM by Th5;
hence J,v |= Suc (f ^ <*VERUM*>) by VALUAT_1:32; :: thesis: verum