now ( F2() <> {} implies P1[F2()] )defpred S1[
set ]
means ex
B being
set st
(
B = $1 &
P1[
B] );
assume
F2()
<> {}
;
P1[F2()]consider G being
set such that A4:
for
x being
set holds
(
x in G iff (
x in bool F2() &
S1[
x] ) )
from XFAMILY:sch 1();
G c= bool F2()
by A4;
then reconsider GA =
G as
Subset-Family of
F2() ;
{} c= F2()
;
then
GA <> {}
by A2, A4;
then consider B being
set such that A5:
B in GA
and A6:
for
X being
set st
X in GA &
B c= X holds
B = X
by A1, FINSET_1:6;
A7:
ex
A being
set st
(
A = B &
P1[
A] )
by A4, A5;
now not B <> F2()set x = the
Element of
F2()
\ B;
assume
B <> F2()
;
contradictionthen
not
F2()
c= B
by A5;
then A8:
F2()
\ B <> {}
by XBOOLE_1:37;
then
not the
Element of
F2()
\ B in B
by XBOOLE_0:def 5;
then A9:
B \/ { the Element of F2() \ B} <> B
by XBOOLE_1:7, ZFMISC_1:31;
A10:
the
Element of
F2()
\ B in F2()
by A8, XBOOLE_0:def 5;
then
{ the Element of F2() \ B} c= F2()
by ZFMISC_1:31;
then A11:
B \/ { the Element of F2() \ B} c= F2()
by A5, XBOOLE_1:8;
B is
Subset of
F1()
by A5, XBOOLE_1:1;
then
B \/ { the Element of F2() \ B} in GA
by A4, A11, A3, A5, A7, A10;
hence
contradiction
by A6, A9, XBOOLE_1:7;
verum end; hence
P1[
F2()]
by A7;
verum end;
hence
P1[F2()]
by A2; verum