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