let Al be QC-alphabet ; :: thesis: for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A)
for f being FinSequence of CQC-WFF Al st len f > 0 holds
( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f )

let A be non empty set ; :: thesis: for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A)
for f being FinSequence of CQC-WFF Al st len f > 0 holds
( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f )

let J be interpretation of Al,A; :: thesis: for v being Element of Valuations_in (Al,A)
for f being FinSequence of CQC-WFF Al st len f > 0 holds
( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f )

let v be Element of Valuations_in (Al,A); :: thesis: for f being FinSequence of CQC-WFF Al st len f > 0 holds
( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f )

let f be FinSequence of CQC-WFF Al; :: thesis: ( len f > 0 implies ( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f ) )
assume A1: len f > 0 ; :: thesis: ( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f )
thus ( J,v |= Ant f & J,v |= Suc f implies J,v |= f ) :: thesis: ( J,v |= f implies ( J,v |= Ant f & J,v |= Suc f ) )
proof
assume that
A2: J,v |= Ant f and
A3: J,v |= Suc f ; :: thesis: J,v |= f
let p be Element of CQC-WFF Al; :: according to CALCUL_1:def 11,CALCUL_1:def 14 :: thesis: ( p in rng f implies J,v |= p )
assume p in rng f ; :: thesis: J,v |= p
then p in (rng (Ant f)) \/ {(Suc f)} by ;
then A4: ( p in rng (Ant f) or p in {(Suc f)} ) by XBOOLE_0:def 3;
J,v |= rng (Ant f) by A2;
hence J,v |= p by ; :: thesis: verum
end;
thus ( J,v |= f implies ( J,v |= Ant f & J,v |= Suc f ) ) :: thesis: verum
proof
assume A5: J,v |= rng f ; :: according to CALCUL_1:def 14 :: thesis: ( J,v |= Ant f & J,v |= Suc f )
thus J,v |= rng (Ant f) :: according to CALCUL_1:def 14 :: thesis: J,v |= Suc f
proof
A6: rng (Ant f) c= (rng (Ant f)) \/ {(Suc f)} by XBOOLE_1:7;
let p be Element of CQC-WFF Al; :: according to CALCUL_1:def 11 :: thesis: ( p in rng (Ant f) implies J,v |= p )
assume p in rng (Ant f) ; :: thesis: J,v |= p
then p in (rng (Ant f)) \/ {(Suc f)} by A6;
then p in rng f by ;
hence J,v |= p by A5; :: thesis: verum
end;
0 + 1 <= len f by ;
then A7: len f in dom f by FINSEQ_3:25;
Suc f = f . (len f) by ;
then Suc f in rng f by ;
hence J,v |= Suc f by A5; :: thesis: verum
end;