let A be QC-alphabet ; :: thesis: for p, q, p1 being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st p1 is_an_universal_closure_of p holds
( X \/ {p} |- q iff X |- p1 => q )
let p, q, p1 be Element of CQC-WFF A; :: thesis: for X being Subset of (CQC-WFF A) st p1 is_an_universal_closure_of p holds
( X \/ {p} |- q iff X |- p1 => q )
let X be Subset of (CQC-WFF A); :: 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 :: thesis: ( X \/ {p} |- q implies X |- p1 => q )
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;
hence X |- p1 => q by A3, CQC_THE2:92; :: thesis: verum
end;
hence ( X \/ {p} |- q implies X |- p1 => q ) ; :: thesis: ( X |- p1 => q implies X \/ {p} |- q )
now :: thesis: ( X |- p1 => q implies X \/ {p} |- q )
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