let
x
be
Element
of
Class
F
_{2}
();
:: thesis:
P
_{1}
[
x
]
ex
y
being
object
st
(
y
in
F
_{1}
() &
x
=
Class
(
F
_{2}
(),
y
) )
by
EQREL_1:def 3
;
hence
P
_{1}
[
x
]
by
A1
;
:: thesis:
verum