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