let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al holds

( p in Cn X iff ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) )

let X be Subset of (CQC-WFF Al); :: thesis: for p being Element of CQC-WFF Al holds

( p in Cn X iff ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) )

let p be Element of CQC-WFF Al; :: thesis: ( p in Cn X iff ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) )

thus ( p in Cn X implies ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) ) :: thesis: ( ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) implies p in Cn X )

( f is_a_proof_wrt X & Effect f = p ) implies p in Cn X ) :: thesis: verum

for p being Element of CQC-WFF Al holds

( p in Cn X iff ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) )

let X be Subset of (CQC-WFF Al); :: thesis: for p being Element of CQC-WFF Al holds

( p in Cn X iff ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) )

let p be Element of CQC-WFF Al; :: thesis: ( p in Cn X iff ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) )

thus ( p in Cn X implies ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) ) :: thesis: ( ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) implies p in Cn X )

proof

thus
( ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
assume
p in Cn X
; :: thesis: ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p )

then p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } by Th31;

then ex F being Element of CQC-WFF Al st

( F = p & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) ) ;

hence ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) ; :: thesis: verum

end;( f is_a_proof_wrt X & Effect f = p )

then p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } by Th31;

then ex F being Element of CQC-WFF Al st

( F = p & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) ) ;

hence ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = p ) ; :: thesis: verum

( f is_a_proof_wrt X & Effect f = p ) implies p in Cn X ) :: thesis: verum

proof

given f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] such that A1:
( f is_a_proof_wrt X & Effect f = p )
; :: thesis: p in Cn X

p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } by A1;

hence p in Cn X by Th31; :: thesis: verum

end;p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st

( f is_a_proof_wrt X & Effect f = F ) } by A1;

hence p in Cn X by Th31; :: thesis: verum