let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A
for X, Y being Subset of (CQC-WFF A) st X |- p & X c= Y holds
Y |- p
let p be Element of CQC-WFF A; :: thesis: for X, Y being Subset of (CQC-WFF A) st X |- p & X c= Y holds
Y |- p
let X, Y be Subset of (CQC-WFF A); :: thesis: ( X |- p & X c= Y implies Y |- p )
assume that
A1: X |- p and
A2: X c= Y ; :: thesis: Y |- p
A3: p in Cn X by A1, CQC_THE1:def 8;
Cn X c= Cn Y by A2, CQC_THE1:18;
hence Y |- p by A3, CQC_THE1:def 8; :: thesis: verum