let S be non empty set ; :: thesis: for R being total Relation of ,
for s being Element of S
for BASSIGN being non empty Subset of
for f, g being Assign of (CTLModel R,BASSIGN) holds
( s |= f 'or' g iff ( s |= f or s |= g ) )
let R be total Relation of ,; :: thesis: for s being Element of S
for BASSIGN being non empty Subset of
for f, g being Assign of (CTLModel R,BASSIGN) holds
( s |= f 'or' g iff ( s |= f or s |= g ) )
let s be Element of S; :: thesis: for BASSIGN being non empty Subset of
for f, g being Assign of (CTLModel R,BASSIGN) holds
( s |= f 'or' g iff ( s |= f or s |= g ) )
let BASSIGN be non empty Subset of ; :: thesis: for f, g being Assign of (CTLModel R,BASSIGN) holds
( s |= f 'or' g iff ( s |= f or s |= g ) )
let f, g be Assign of (CTLModel R,BASSIGN); :: thesis: ( s |= f 'or' g iff ( s |= f or s |= g ) )
( s |= f 'or' g iff not s |= ('not' f) '&' ('not' g) ) by Th12;
then ( s |= f 'or' g iff ( not s |= 'not' f or not s |= 'not' g ) ) by Th13;
hence ( s |= f 'or' g iff ( s |= f or s |= g ) ) by Th12; :: thesis: verum