let R be non empty connected Poset; :: thesis: for n being Element of 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 Element of 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 a' = a as finite set ;

now

let w be set ; :: thesis: ( w in {(PosetMax a)} implies w in a )
assume A2: w in {(PosetMax a)} ; :: thesis: w in a
w = PosetMax a by A2, TARSKI:def 1;
hence w in a by A1, Def15, CARD_1:47; :: thesis: verum

end;

then {(PosetMax a)} c= a by TARSKI:def 3;
then A3: card (a' \ {(PosetMax a)}) = (card a') - (card {(PosetMax a)}) by CARD_2:63;
card {(PosetMax a)} = 1 by CARD_1:50;
hence card (a \ {(PosetMax a)}) = n by A1, A3; :: thesis: verum