e
[e1,e2].P[e] == e:E. (e1 
loc e 
e loc e2 P[e])
Definitions :
all: x:A. B[x],
es-E: E,
implies: P Q,
es-le: e loc e'
FDL editor aliases :
alle-between2
\mforall{}e\mmember{}[e1,e2].P[e] == \mforall{}e:E. (e1 \mleq{}loc e {}\mRightarrow{} e \mleq{}loc e2 {}\mRightarrow{} P[e])
Date html generated:
2010_08_27-AM-09_28_48
Last ObjectModification:
2009_12_16-AM-01_04_01
Home
Index