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

A1: now

assume X |-| Y ; :: thesis: Cn X = Cn Y
then ( X |- Y & Y |- X ) by Th18;
then ( Y c= Cn X & X c= Cn Y ) by Th7;
then ( Cn Y c= Cn X & Cn X c= Cn Y ) by CQC_THE1:36, CQC_THE1:37;
hence Cn X = Cn Y by XBOOLE_0:def 10; :: thesis: verum

end;

now

assume A2: Cn X = Cn Y ; :: thesis: X |-| Y
( Y c= Cn Y & X c= Cn X ) by CQC_THE1:38;
then ( X |- Y & Y |- X ) by A2, Th7;
hence X |-| Y by Th18; :: thesis: verum

end;

hence ( X |-| Y iff Cn X = Cn Y ) by A1; :: thesis: verum