let X be Subset of CQC-WFF ; :: thesis: for p being Element of CQC-WFF holds
( p in Cn X iff ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = p ) )
let p be Element of CQC-WFF ; :: thesis: ( p in Cn X iff ex f being FinSequence of [:CQC-WFF ,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 ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = p ) ) :: thesis: ( ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = p ) implies p in Cn X )

proof

assume A1: p in Cn X ; :: thesis: ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = p )
A2: p in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = F ) } by A1, Th69;
A3: ex F being Element of CQC-WFF st
( F = p & ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = F ) ) by A2;
thus ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = p ) by A3; :: thesis: verum

end;

thus ( ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = p ) implies p in Cn X ) :: thesis: verum

proof

given f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] such that A4: ( f is_a_proof_wrt X & Effect f = p ) ; :: thesis: p in Cn X
A5: p in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt X & Effect f = F ) } by A4;
thus p in Cn X by A5, Th69; :: thesis: verum

end;