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