let C1, C2 be Subset of the carrier' of X; :: thesis: ( s in C1 & ( for e being Element of X
for s1 being stack of X st s1 in C1 holds
( push (e,s1) in C1 & ( not emp s1 implies pop s1 in C1 ) ) ) & ( for A being Subset of the carrier' of X st s in A & ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) holds
C1 c= A ) & s in C2 & ( for e being Element of X
for s1 being stack of X st s1 in C2 holds
( push (e,s1) in C2 & ( not emp s1 implies pop s1 in C2 ) ) ) & ( for A being Subset of the carrier' of X st s in A & ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) holds
C2 c= A ) implies C1 = C2 )
assume A1: ( s in C1 & ( for e being Element of X
for s1 being stack of X st s1 in C1 holds
( push (e,s1) in C1 & ( not emp s1 implies pop s1 in C1 ) ) ) & ( for A being Subset of the carrier' of X st s in A & ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) holds
C1 c= A ) & s in C2 & ( for e being Element of X
for s1 being stack of X st s1 in C2 holds
( push (e,s1) in C2 & ( not emp s1 implies pop s1 in C2 ) ) ) & ( for A being Subset of the carrier' of X st s in A & ( for e being Element of X
for s1 being stack of X st s1 in A holds
( push (e,s1) in A & ( not emp s1 implies pop s1 in A ) ) ) holds
C2 c= A ) & not C1 = C2 ) ; :: thesis: contradiction
C1 = C2

proof

thus ( C1 c= C2 & C2 c= C1 ) by A1; :: according to XBOOLE_0:def 10 :: thesis: verum

end;

hence contradiction by A1; :: thesis: verum