let Al be QC-alphabet ; :: thesis: for f, g being FinSequence of CQC-WFF Al st len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & Ant f |= Suc f & Ant g |= Suc g holds
Ant (Ant f) |= Suc f
let f, g be FinSequence of CQC-WFF Al; :: thesis: ( len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & Ant f |= Suc f & Ant g |= Suc g implies Ant (Ant f) |= Suc f )
assume that
A1: len f > 1 and
A2: len g > 1 and
A3: Ant (Ant f) = Ant (Ant g) and
A4: 'not' (Suc (Ant f)) = Suc (Ant g) and
A5: Suc f = Suc g and
A6: Ant f |= Suc f and
A7: Ant g |= Suc g ; :: thesis: Ant (Ant f) |= Suc f
let A be non empty set ; :: according to CALCUL_1:def 15 :: thesis: for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= Ant (Ant f) holds
J,v |= Suc f
let J be interpretation of Al,A; :: thesis: for v being Element of Valuations_in (Al,A) st J,v |= Ant (Ant f) holds
J,v |= Suc f
let v be Element of Valuations_in (Al,A); :: thesis: ( J,v |= Ant (Ant f) implies J,v |= Suc f )
assume A8: J,v |= Ant (Ant f) ; :: thesis: J,v |= Suc f
A9: len (Ant g) > 0 by A2, Th4;

A10: now :: thesis: ( not J,v |= Suc (Ant f) implies J,v |= Suc f )

assume not J,v |= Suc (Ant f) ; :: thesis: J,v |= Suc f
then J,v |= Suc (Ant g) by A4, VALUAT_1:17;
then J,v |= Ant g by A3, A9, A8, Th17;
hence J,v |= Suc f by A5, A7; :: thesis: verum

end;

A11: len (Ant f) > 0 by A1, Th4;

now :: thesis: ( J,v |= Suc (Ant f) implies J,v |= Suc f )

assume J,v |= Suc (Ant f) ; :: thesis: J,v |= Suc f
then J,v |= Ant f by A11, A8, Th17;
hence J,v |= Suc f by A6; :: thesis: verum

end;

hence J,v |= Suc f by A10; :: thesis: verum