let A be QC-alphabet ; :: thesis: for X, Y being Subset of (CQC-WFF A) holds
( X |-| Y iff ( X |- Y & Y |- X ) )
let X, Y be Subset of (CQC-WFF A); :: thesis: ( X |-| Y iff ( X |- Y & Y |- X ) )

A1: now :: thesis: ( X |- Y & Y |- X implies X |-| Y )

assume that
A2: X |- Y and
A3: Y |- X ; :: thesis: X |-| Y

now :: thesis: for p being Element of CQC-WFF A holds
( X |- p iff Y |- p )

let p be Element of CQC-WFF A; :: thesis: ( X |- p iff Y |- p )

A4: now :: thesis: ( Y |- p implies X |- p )

assume Y |- p ; :: thesis: X |- p
then Y |- {p} by Th10;
then X |- {p} by A2, Th9;
hence X |- p by Th10; :: thesis: verum

end;

now :: thesis: ( X |- p implies Y |- p )

assume X |- p ; :: thesis: Y |- p
then X |- {p} by Th10;
then Y |- {p} by A3, Th9;
hence Y |- p by Th10; :: thesis: verum

end;

hence ( X |- p iff Y |- p ) by A4; :: thesis: verum

end;

hence X |-| Y by Def4; :: thesis: verum

end;

now :: thesis: ( X |-| Y implies ( X |- Y & Y |- X ) )

assume A5: X |-| Y ; :: thesis: ( X |- Y & Y |- X )

now :: thesis: for p being Element of CQC-WFF A st p in Y holds
X |- p

let p be Element of CQC-WFF A; :: thesis: ( p in Y implies X |- p )
assume p in Y ; :: thesis: X |- p
then Y |- p by Th1;
hence X |- p by A5, Def4; :: thesis: verum

end;

hence X |- Y by Def2; :: thesis: Y |- X

now :: thesis: for p being Element of CQC-WFF A st p in X holds
Y |- p

let p be Element of CQC-WFF A; :: thesis: ( p in X implies Y |- p )
assume p in X ; :: thesis: Y |- p
then X |- p by Th1;
hence Y |- p by A5, Def4; :: thesis: verum

end;

hence Y |- X by Def2; :: thesis: verum

end;

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