:: deftheorem Def2 defines positive PELLS_EQ:def 2 :
for D1, D2 being non empty real-membered set
for p being Element of [:D1,D2:] holds
( p is positive iff ( p `1 is positive & p `2 is positive ) );