consider EQR being Equivalence_Relation of X such that
A1: S1 = Class EQR by Th43;
take Class EQR,x ; :: thesis: ( x in Class EQR,x & Class EQR,x in S1 )
thus x in Class EQR,x by Th28; :: thesis: Class EQR,x in S1
thus Class EQR,x in S1 by A1, Def5; :: thesis: verum