let A be QC-alphabet ; :: thesis: for X, Y being Subset of (CQC-WFF A) holds
( X |-| Y iff Cn X = Cn Y )
let X, Y be Subset of (CQC-WFF A); :: thesis: ( X |-| Y iff Cn X = Cn Y )
A1: now :: thesis: ( X |-| Y implies Cn X = Cn Y )
assume A2: X |-| Y ; :: thesis: Cn X = Cn Y
then Y |- X by Th18;
then X c= Cn Y by Th7;
then A3: Cn X c= Cn Y by CQC_THE1:15, CQC_THE1:16;
X |- Y by A2, Th18;
then Y c= Cn X by Th7;
then Cn Y c= Cn X by CQC_THE1:15, CQC_THE1:16;
hence Cn X = Cn Y by A3, XBOOLE_0:def 10; :: thesis: verum
end;
now :: thesis: ( Cn X = Cn Y implies X |-| Y )
assume A4: Cn X = Cn Y ; :: thesis: X |-| Y
X c= Cn X by CQC_THE1:17;
then A5: Y |- X by A4, Th7;
Y c= Cn Y by CQC_THE1:17;
then X |- Y by A4, Th7;
hence X |-| Y by A5, Th18; :: thesis: verum
end;
hence ( X |-| Y iff Cn X = Cn Y ) by A1; :: thesis: verum