let X, Y be Subset of CQC-WFF ; :: thesis: for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A st J,v |= X & Y c= X holds
J,v |= Y
let A be non empty set ; :: thesis: for J being interpretation of A
for v being Element of Valuations_in A st J,v |= X & Y c= X holds
J,v |= Y
let J be interpretation of A; :: thesis: for v being Element of Valuations_in A st J,v |= X & Y c= X holds
J,v |= Y
let v be Element of Valuations_in 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 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