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

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