theorem Th65:
for
X being
set st
X <> {} & ( for
Z being
set st
Z c= X &
Z is
c=-linear holds
ex
Y being
set st
(
Y in X & ( for
X1 being
set st
X1 in Z holds
X1 c= Y ) ) ) holds
ex
Y being
set st
(
Y in X & ( for
Z being
set st
Z in X &
Z <> Y holds
not
Y c= Z ) )