let X be StackAlgebra; for s being stack of X
for S being stack of (X /==) st S = Class ((==_ X),s) & not emp s holds
top S = top s
let s be stack of X; for S being stack of (X /==) st S = Class ((==_ X),s) & not emp s holds
top S = top s
set t = the s_top of X;
set A = the s_empty of X;
set e = the Element of the carrier of X;
let S be stack of (X /==); ( S = Class ((==_ X),s) & not emp s implies top S = top s )
assume Z0:
S = Class ((==_ X),s)
; ( emp s or top S = top s )
assume Z1:
not emp s
; top S = top s
then
not emp S
by Z0, Th71;
then A2:
S <> the s_empty of X
by Th71a;
set f = the Choice_Function of Class (==_ X);
A4:
( S in Class (==_ X) & {} nin Class (==_ X) )
by Z0, EQREL_1:def 3, SETFAM_1:def 8;
then A3:
the Choice_Function of Class (==_ X) . S in S
by ORDERS_1:def 1;
then reconsider x = the Choice_Function of Class (==_ X) . S as stack of X by Z0;
[s,x] in ==_ X
by Z0, A3, EQREL_1:18;
then A6:
s == x
by REL;
A5:
dom the Choice_Function of Class (==_ X) = Class (==_ X)
by A4, RLVECT_3:28;
the s_top of (X /==) = ( the s_top of X * the Choice_Function of Class (==_ X)) +* ( the s_empty of X, the Element of the carrier of X)
by QUOT;
hence top S =
( the s_top of X * the Choice_Function of Class (==_ X)) . S
by A2, FUNCT_7:32
.=
top x
by A4, A5, FUNCT_1:13
.=
top s
by A6, Z1, Th46
;
verum