let H1, H2 be CTL-formula; :: thesis: for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF ,the BasicAssign of (CTLModel R,BASSIGN) holds
( s,kai |= H1 'or' H2 iff ( s,kai |= H1 or s,kai |= H2 ) )
let S be non empty set ; :: thesis: for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF ,the BasicAssign of (CTLModel R,BASSIGN) holds
( s,kai |= H1 'or' H2 iff ( s,kai |= H1 or s,kai |= H2 ) )
let R be total Relation of S,S; :: thesis: for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF ,the BasicAssign of (CTLModel R,BASSIGN) holds
( s,kai |= H1 'or' H2 iff ( s,kai |= H1 or s,kai |= H2 ) )
let s be Element of S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF ,the BasicAssign of (CTLModel R,BASSIGN) holds
( s,kai |= H1 'or' H2 iff ( s,kai |= H1 or s,kai |= H2 ) )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for kai being Function of atomic_WFF ,the BasicAssign of (CTLModel R,BASSIGN) holds
( s,kai |= H1 'or' H2 iff ( s,kai |= H1 or s,kai |= H2 ) )
let kai be Function of atomic_WFF ,the BasicAssign of (CTLModel R,BASSIGN); :: thesis: ( s,kai |= H1 'or' H2 iff ( s,kai |= H1 or s,kai |= H2 ) )
( s,kai |= H1 'or' H2 iff s |= Evaluate (H1 'or' H2),kai ) by Def60;
then ( s,kai |= H1 'or' H2 iff s |= (Evaluate H1,kai) 'or' (Evaluate H2,kai) ) by Th10;
then ( s,kai |= H1 'or' H2 iff ( s |= Evaluate H1,kai or s |= Evaluate H2,kai ) ) by Th17;
hence ( s,kai |= H1 'or' H2 iff ( s,kai |= H1 or s,kai |= H2 ) ) by Def60; :: thesis: verum