let Al be QC-alphabet ; :: thesis: for X, Y being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st X |- p & X c= Y holds
Y |- p
let X, Y be Subset of (CQC-WFF Al); :: thesis: for p being Element of CQC-WFF Al st X |- p & X c= Y holds
Y |- p
let p be Element of CQC-WFF Al; :: thesis: ( X |- p & X c= Y implies Y |- p )
assume that
A1: X |- p and
A2: X c= Y ; :: thesis: Y |- p
consider f being FinSequence of CQC-WFF Al such that
A3: rng f c= X and
A4: |- f ^ <*p*> by A1, HENMODEL:def 1;
rng f c= Y by A2, A3;
hence Y |- p by A4, HENMODEL:def 1; :: thesis: verum