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