let X be Subset of CQC-WFF ; :: thesis: for p, q being Element of CQC-WFF holds
( ( X |- p & X |- q ) iff X |- p '&' q )
let p, q be Element of CQC-WFF ; :: thesis: ( ( X |- p & X |- q ) iff X |- p '&' q )
thus ( X |- p & X |- q implies X |- p '&' q ) :: thesis: ( X |- p '&' q implies ( X |- p & X |- q ) )

proof

assume A1: ( X |- p & X |- q ) ; :: thesis: X |- p '&' q
then consider f1 being FinSequence of CQC-WFF such that
A2: ( rng f1 c= X & |- f1 ^ <*p*> ) by HENMODEL:def 2;
consider f2 being FinSequence of CQC-WFF such that
A3: ( rng f2 c= X & |- f2 ^ <*q*> ) by A1, HENMODEL:def 2;
( |- (f1 ^ f2) ^ <*p*> & |- (f1 ^ f2) ^ <*q*> ) by A2, A3, CALCUL_2:20, HENMODEL:5;
then A4: |- (f1 ^ f2) ^ <*(p '&' q)*> by Th5;
rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:44;
then rng (f1 ^ f2) c= X by A2, A3, XBOOLE_1:8;
hence X |- p '&' q by A4, HENMODEL:def 2; :: thesis: verum

end;

thus ( X |- p '&' q implies ( X |- p & X |- q ) ) :: thesis: verum

proof

assume X |- p '&' q ; :: thesis: ( X |- p & X |- q )
then consider f1 being FinSequence of CQC-WFF such that
A5: ( rng f1 c= X & |- f1 ^ <*(p '&' q)*> ) by HENMODEL:def 2;
( |- f1 ^ <*p*> & |- f1 ^ <*q*> ) by A5, CALCUL_2:22, CALCUL_2:23;
hence ( X |- p & X |- q ) by A5, HENMODEL:def 2; :: thesis: verum

end;