set IT = R quotient (E,F);
now :: thesis: for x being object st x in R quotient (E,F) holds
x in [:(Class E),(Class F):]
let x be object ; :: thesis: ( x in R quotient (E,F) implies x in [:(Class E),(Class F):] )
assume x in R quotient (E,F) ; :: thesis: x in [:(Class E),(Class F):]
then consider e being Element of Class E, f being Element of Class F such that
A1: ( x = [e,f] & ex x, y being set st
( x in e & y in f & [x,y] in R ) ) ;
thus x in [:(Class E),(Class F):] by A1; :: thesis: verum
end;
hence R quotient (E,F) is Relation of (Class E),(Class F) by TARSKI:def 3; :: thesis: verum