:: deftheorem Def2 defines plain GLIBPRE0:def 2 :
for GF being non empty Graph-yielding Function holds
( GF is plain iff for x being Element of dom GF holds GF . x is plain );