:: deftheorem Def44 defines EneXt_univ MODELC_1:def 44 :
for S being non empty set
for R being total Relation of S,S
for f being Function of S,BOOLEAN
for x being object holds
( ( x in S & ex pai being inf_path of R st
( pai . 0 = x & f . (pai . 1) = TRUE ) implies EneXt_univ (x,f,R) = TRUE ) & ( ( not x in S or for pai being inf_path of R holds
( not pai . 0 = x or not f . (pai . 1) = TRUE ) ) implies EneXt_univ (x,f,R) = FALSE ) );