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

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