let H1, H2 be CTL-formula; :: thesis: for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((H1 'or' H2),Kai) = (Evaluate (H1,Kai)) 'or' (Evaluate (H2,Kai))
let V be CTLModel; :: thesis: for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((H1 'or' H2),Kai) = (Evaluate (H1,Kai)) 'or' (Evaluate (H2,Kai))
let Kai be Function of atomic_WFF, the BasicAssign of V; :: thesis: Evaluate ((H1 'or' H2),Kai) = (Evaluate (H1,Kai)) 'or' (Evaluate (H2,Kai))
Evaluate ((H1 'or' H2),Kai) = 'not' (Evaluate ((('not' H1) '&' ('not' H2)),Kai)) by Th5
.= 'not' ((Evaluate (('not' H1),Kai)) '&' (Evaluate (('not' H2),Kai))) by Th6
.= 'not' (('not' (Evaluate (H1,Kai))) '&' (Evaluate (('not' H2),Kai))) by Th5 ;
hence Evaluate ((H1 'or' H2),Kai) = (Evaluate (H1,Kai)) 'or' (Evaluate (H2,Kai)) by Th5; :: thesis: verum