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 ;

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

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

then
{(PosetMax a)} c= a
;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;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

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