let A be non empty set ; :: thesis: for s being stack of (StandardStackSystem A) holds |.s.| = s
defpred S₁[ stack of (StandardStackSystem A)] means |.$1.| = $1;

A1: now :: thesis: for s being stack of (StandardStackSystem A) st emp s holds
S₁[s]

let s be stack of (StandardStackSystem A); :: thesis: ( emp s implies S₁[s] )
assume emp s ; :: thesis: S₁[s]
then ( s = {} & |.s.| = {} ) by Def7, Th5;
hence S₁[s] ; :: thesis: verum

end;

A2: now :: thesis: for s being stack of (StandardStackSystem A)
for e being Element of (StandardStackSystem A) st S₁[s] holds
S₁[ push (e,s)]

let s be stack of (StandardStackSystem A); :: thesis: for e being Element of (StandardStackSystem A) st S₁[s] holds
S₁[ push (e,s)]
let e be Element of (StandardStackSystem A); :: thesis: ( S₁[s] implies S₁[ push (e,s)] )
assume S₁[s] ; :: thesis: S₁[ push (e,s)]
then |.(push (e,s)).| = <*e*> ^ s by Th8;
hence S₁[ push (e,s)] by Def7; :: thesis: verum

end;

let s be stack of (StandardStackSystem A); :: thesis: |.s.| = s
thus S₁[s] from STACKS_1:sch 3(A1, A2); :: thesis: verum