let R be non empty connected Poset; :: thesis: for n being Nat
for a being Element of Fin the carrier of R st card a = n + 1 holds
card (a \ {(PosetMax a)}) = n
let n be Nat; :: thesis: for a being Element of Fin the carrier of R st card a = n + 1 holds
card (a \ {(PosetMax a)}) = n
let a be Element of Fin the carrier of R; :: thesis: ( card a = n + 1 implies card (a \ {(PosetMax a)}) = n )
assume A1: card a = n + 1 ; :: thesis: card (a \ {(PosetMax a)}) = n
reconsider a9 = a as finite set ;

now :: thesis: for w being object st w in {(PosetMax a)} holds
w in a

let w be object ; :: thesis: ( w in {(PosetMax a)} implies w in a )
assume w in {(PosetMax a)} ; :: thesis: w in a
then w = PosetMax a by TARSKI:def 1;
hence w in a by A1, Def13, CARD_1:27; :: thesis: verum

end;

then {(PosetMax a)} c= a ;
then A2: card (a9 \ {(PosetMax a)}) = (card a9) - (card {(PosetMax a)}) by CARD_2:44;
card {(PosetMax a)} = 1 by CARD_1:30;
hence card (a \ {(PosetMax a)}) = n by A1, A2; :: thesis: verum