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 ) )
thus ( X |-| Y implies ( X |- Y & Y |- X ) ) by Th1; :: thesis: ( X |- Y & Y |- X implies X |-| Y )
assume that
A1: X |- Y and
A2: Y |- X ; :: thesis: X |-| Y
let p be Element of CQC-WFF A; :: according to CQC_THE3:def 4 :: thesis: ( X |- p iff Y |- p )
A3: now :: thesis: ( Y |- p implies X |- p )
assume Y |- p ; :: thesis: X |- p
then Y |- {p} by Th10;
then X |- {p} by A1, 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 A2, Th9;
hence Y |- p by Th10; :: thesis: verum
end;
hence ( X |- p iff Y |- p ) by A3; :: thesis: verum