per cases ( Y c= NAT or not Y c= NAT ) ;

suppose Y c= NAT ; :: thesis: ex b₁ being QC-symbol of A st
( b₁ in Y & ( for t being QC-symbol of A st t in Y holds
b₁ <= t ) )

then reconsider Y = Y as non empty Subset of NAT ;
set y = min* Y;
NAT c= QC-symbols A by Th3;
then reconsider yp = min* Y as QC-symbol of A ;
take yp ; :: thesis: ( yp in Y & ( for t being QC-symbol of A st t in Y holds
yp <= t ) )
for t being QC-symbol of A st t in Y holds
yp <= t

proof

let t be QC-symbol of A; :: thesis: ( t in Y implies yp <= t )
assume A1: t in Y ; :: thesis: yp <= t
reconsider t = t as Nat by A1;
min* Y <= t by A1, NAT_1:def 1;
hence yp <= t by A1, Def33; :: thesis: verum

end;

hence ( yp in Y & ( for t being QC-symbol of A st t in Y holds
yp <= t ) ) by NAT_1:def 1; :: thesis: verum

end;

suppose not Y c= NAT ; :: thesis: ex b₁ being QC-symbol of A st
( b₁ in Y & ( for t being QC-symbol of A st t in Y holds
b₁ <= t ) )

then consider a being object such that
A2: ( a in Y & not a in NAT ) ;
set R = the Relation of A;
( the Relation of A well_orders (QC-symbols A) \ NAT & Y \ NAT <> {} ) by A2, Def32, XBOOLE_0:def 5;
then consider y being object such that
A3: ( y in Y \ NAT & ( for b being object st b in Y \ NAT holds
[y,b] in the Relation of A ) ) by WELLORD1:5, XBOOLE_1:33;
reconsider y = y as QC-symbol of A by A3;
A4: ( not y in NAT & y in Y ) by A3, XBOOLE_0:def 5;
for s being QC-symbol of A st s in Y holds
y <= s

proof

let s be QC-symbol of A; :: thesis: ( s in Y implies y <= s )
assume A5: s in Y ; :: thesis: y <= s

per cases ( s in NAT or not s in NAT ) ;

suppose s in NAT ; :: thesis: y <= s

hence y <= s by A4, Def33; :: thesis: verum

end;

suppose A6: not s in NAT ; :: thesis: y <= s

then s in Y \ NAT by A5, XBOOLE_0:def 5;
then [y,s] in the Relation of A by A3;
hence y <= s by A4, A6, Def33; :: thesis: verum

end;

end;

end;

hence ex b₁ being QC-symbol of A st
( b₁ in Y & ( for t being QC-symbol of A st t in Y holds
b₁ <= t ) ) by A4; :: thesis: verum

end;

end;