let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)
for p, q being Element of CQC-WFF Al holds
( ( X |- p & X |- q ) iff X |- p '&' q )
let X be Subset of (CQC-WFF Al); :: thesis: for p, q being Element of CQC-WFF Al holds
( ( X |- p & X |- q ) iff X |- p '&' q )
let p, q be Element of CQC-WFF Al; :: 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 that
A1: X |- p and
A2: X |- q ; :: thesis: X |- p '&' q
consider f1 being FinSequence of CQC-WFF Al such that
A3: rng f1 c= X and
A4: |- f1 ^ <*p*> by A1, HENMODEL:def 1;
consider f2 being FinSequence of CQC-WFF Al such that
A5: rng f2 c= X and
A6: |- f2 ^ <*q*> by A2, HENMODEL:def 1;
A7: |- (f1 ^ f2) ^ <*p*> by A4, HENMODEL:5;
|- (f1 ^ f2) ^ <*q*> by A6, CALCUL_2:20;
then A8: |- (f1 ^ f2) ^ <*(p '&' q)*> by A7, Th5;
rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31;
then rng (f1 ^ f2) c= X by A3, A5, XBOOLE_1:8;
hence X |- p '&' q by A8, HENMODEL:def 1; :: 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 Al such that
A9: rng f1 c= X and
A10: |- f1 ^ <*(p '&' q)*> by HENMODEL:def 1;
A11: |- f1 ^ <*p*> by A10, CALCUL_2:22;
|- f1 ^ <*q*> by A10, CALCUL_2:23;
hence ( X |- p & X |- q ) by A9, A11, HENMODEL:def 1; :: thesis: verum
end;