let R be non empty connected Poset; :: thesis: for a being Element of Fin the carrier of R holds a \ {(PosetMax a)} is Element of Fin the carrier of R
let a be Element of Fin the carrier of R; :: thesis: a \ {(PosetMax a)} is Element of Fin the carrier of R
set CR = the carrier of R;
A1: a c= the carrier of R by FINSUB_1:def 5;
reconsider a9 = a as finite set ;
set z = a9 \ {(PosetMax a)};
a9 \ {(PosetMax a)} c= the carrier of R by A1;
hence a \ {(PosetMax a)} is Element of Fin the carrier of R by FINSUB_1:def 5; :: thesis: verum