let A be non empty set ; :: thesis: for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF holds Val_S v,S = Val_S v,(Sub_not S)
let v be Element of Valuations_in A; :: thesis: for S being Element of CQC-Sub-WFF holds Val_S v,S = Val_S v,(Sub_not S)
let S be Element of CQC-Sub-WFF ; :: thesis: Val_S v,S = Val_S v,(Sub_not S)
Sub_not S = [('not' (S `1 )),(S `2 )] by SUBSTUT1:def 20;
hence Val_S v,S = Val_S v,(Sub_not S) by MCART_1:7; :: thesis: verum