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):]

hence
R quotient (E,F) is Relation of (Class E),(Class F)
by TARSKI:def 3; :: thesis: verumx 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;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