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 *>)
( Ant (f ^ <*VERUM *>) = f & Suc (f ^ <*VERUM *>) = VERUM ) by Th5;
hence J,v |= Suc (f ^ <*VERUM *>) by VALUAT_1:44; :: thesis: verum