let X, Y be Subset of CQC-WFF; :: thesis: ( X |-| Y iff Cn X = Cn Y )

A1: now

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

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