:: deftheorem defines quotient FOMODEL3:def 8 :
for X, Y being non empty set
for E being Equivalence_Relation of X
for F being Equivalence_Relation of Y
for R being Relation holds R quotient (E,F) = { [e,f] where e is Element of Class E, f is Element of Class F : ex x, y being set st
( x in e & y in f & [x,y] in R ) } ;