theorem Th67: :: ORDERS_1:67

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