for R being non empty connected Poset
for a being Element of Fin the carrier of R holds a \ {(PosetMax a)} is Element of Fin the carrier of R