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

A1: now

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

now

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

end;

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

now

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

end;

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

end;

now

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

now

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

A5: now

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

end;

now

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

end;

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

end;

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

end;

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