let p1, p, q be Element of CQC-WFF ; :: thesis: for X being Subset of CQC-WFF st p1 is_an_universal_closure_of p holds
( X \/ {p} |- q iff X |- p1 => q )
let X be Subset of CQC-WFF ; :: thesis: ( p1 is_an_universal_closure_of p implies ( X \/ {p} |- q iff X |- p1 => q ) )
assume A1: p1 is_an_universal_closure_of p ; :: thesis: ( X \/ {p} |- q iff X |- p1 => q )

now

assume X \/ {p} |- q ; :: thesis: X |- p1 => q
then A2: X \/ {p} |- {q} by Th10;
p |-| p1 by A1, Th38;
then {p} |-| {p1} by Th29;
then X \/ {p1} |- {q} by A2, Th26;
then A3: X \/ {p1} |- q by Th10;
p1 is closed by A1, Def6;
hence X |- p1 => q by A3, CQC_THE2:96; :: thesis: verum

end;

hence ( X \/ {p} |- q implies X |- p1 => q ) ; :: thesis: ( X |- p1 => q implies X \/ {p} |- q )

now

assume X |- p1 => q ; :: thesis: X \/ {p} |- q
then X \/ {p1} |- q by Th40;
then A4: X \/ {p1} |- {q} by Th10;
p |-| p1 by A1, Th38;
then {p} |-| {p1} by Th29;
then X \/ {p} |- {q} by A4, Th26;
hence X \/ {p} |- q by Th10; :: thesis: verum

end;

hence ( X |- p1 => q implies X \/ {p} |- q ) ; :: thesis: verum