defpred S1[ set ] means ( s in $1 & ( for e being Element of X
for s1 being stack of X st s1 in $1 holds
( push (e,s1) in $1 & ( not emp s1 implies pop s1 in $1 ) ) ) );
consider Y being set such that
A1: for x being set holds
( x in Y iff ( x in bool the carrier' of X & S1[x] ) ) from XFAMILY:sch 1();
 set S = the carrier' of X;
A2: ( S1[ the carrier' of X] & the carrier' of X in bool the carrier' of X ) by ZFMISC_1:def 1;
then A3: the carrier' of X in Y by A1;
reconsider Y = Y as non empty set by A2, A1;
reconsider C = meet Y as Subset of the carrier' of X by A3, SETFAM_1:3;
take C ; :: thesis: ( s in C & ( for e being Element of X
for s1 being stack of X st s1 in C holds
( push (e,s1) in C & ( not emp s1 implies pop s1 in C ) ) ) & ( 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
C c= A ) )
for x being set st x in Y holds
s in x by A1;
hence s in C by SETFAM_1:def 1; :: thesis: ( ( for e being Element of X
for s1 being stack of X st s1 in C holds
( push (e,s1) in C & ( not emp s1 implies pop s1 in C ) ) ) & ( 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
C c= A ) )
hereby :: thesis: 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
C c= A
let e be Element of X; :: thesis: for s1 being stack of X st s1 in C holds
( push (e,s1) in C & ( not emp s1 implies pop s1 in C ) )
let s1 be stack of X; :: thesis: ( s1 in C implies ( push (e,s1) in C & ( not emp s1 implies pop s1 in C ) ) )
assume A4: s1 in C ; :: thesis: ( push (e,s1) in C & ( not emp s1 implies pop s1 in C ) )
now :: thesis: for x being set st x in Y holds
push (e,s1) in x
let x be set ; :: thesis: ( x in Y implies push (e,s1) in x )
assume A5: x in Y ; :: thesis: push (e,s1) in x
then s1 in x by A4, SETFAM_1:def 1;
hence push (e,s1) in x by A1, A5; :: thesis: verum
end;
hence push (e,s1) in C by SETFAM_1:def 1; :: thesis: ( not emp s1 implies pop s1 in C )
assume A6: not emp s1 ; :: thesis: pop s1 in C
now :: thesis: for x being set st x in Y holds
pop s1 in x
let x be set ; :: thesis: ( x in Y implies pop s1 in x )
assume A7: x in Y ; :: thesis: pop s1 in x
then s1 in x by A4, SETFAM_1:def 1;
hence pop s1 in x by A1, A6, A7; :: thesis: verum
end;
hence pop s1 in C by SETFAM_1:def 1; :: thesis: verum
end;
let A be Subset of the carrier' of X; :: thesis: ( 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 ) ) ) implies C c= A )
assume S1[A] ; :: thesis: C c= A
then A in Y by A1;
hence C c= A by SETFAM_1:3; :: thesis: verum