let Al be QC-alphabet ; :: thesis: {(VERUM Al)} is Consistent
set A = the non empty set ;
set J = the interpretation of Al, the non empty set ;
set v = the Element of Valuations_in (Al, the non empty set );
the interpretation of Al, the non empty set , the Element of Valuations_in (Al, the non empty set ) |= VERUM Al by VALUAT_1:32;
then for p being Element of CQC-WFF Al st p in {(VERUM Al)} holds
the interpretation of Al, the non empty set , the Element of Valuations_in (Al, the non empty set ) |= p by TARSKI:def 1;
then the interpretation of Al, the non empty set , the Element of Valuations_in (Al, the non empty set ) |= {(VERUM Al)} by CALCUL_1:def 11;
hence {(VERUM Al)} is Consistent by Th12; :: thesis: verum