let Al be QC-alphabet ; :: thesis: for X, Y being Subset of (CQC-WFF Al)
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= X & Y c= X holds
J,v |= Y
let X, Y be Subset of (CQC-WFF Al); :: thesis: for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= X & Y c= X holds
J,v |= Y
let A be non empty set ; :: thesis: for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= X & Y c= X holds
J,v |= Y
let J be interpretation of Al,A; :: thesis: for v being Element of Valuations_in (Al,A) st J,v |= X & Y c= X holds
J,v |= Y
let v be Element of Valuations_in (Al,A); :: thesis: ( J,v |= X & Y c= X implies J,v |= Y )
assume A1: J,v |= X ; :: thesis: ( not Y c= X or J,v |= Y )
assume Y c= X ; :: thesis: J,v |= Y
then for p being Element of CQC-WFF Al st p in Y holds
J,v |= p by A1, CALCUL_1:def 11;
hence J,v |= Y by CALCUL_1:def 11; :: thesis: verum