consider
A9
,
B9
being
Subset
of
X
such that
A1
:
A
=
[
A9
,
B9
]
by
Th55
;
thus
A
`1
is
Subset
of
X
by
A1
;
:: thesis:
verum