:: deftheorem Def52 defines EUntill_univ MODELC_1:def 52 :
for S being non empty set
for R being total Relation of S,S
for f, g being Function of S,BOOLEAN
for x being set holds
( ( x in S & ex pai being inf_path of R st
( pai . 0 = x & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
f . (pai . j) = TRUE ) & g . (pai . m) = TRUE ) ) implies EUntill_univ (x,f,g,R) = TRUE ) & ( ( not x in S or for pai being inf_path of R holds
( not pai . 0 = x or for m being Element of NAT holds
( ex j being Element of NAT st
( j < m & not f . (pai . j) = TRUE ) or not g . (pai . m) = TRUE ) ) ) implies EUntill_univ (x,f,g,R) = FALSE ) );