let A be QC-alphabet ; :: thesis: for X, Y being Subset of (CQC-WFF A) st X c= Y holds
Y |- X
let X, Y be Subset of (CQC-WFF A); :: thesis: ( X c= Y implies Y |- X )
assume X c= Y ; :: thesis: Y |- X
then for p being Element of CQC-WFF A st p in X holds
Y |- p by Th1;
hence Y |- X by Def2; :: thesis: verum