set e = { t where t is QC-symbol of A : s < t } ;
A1: { t where t is QC-symbol of A : s < t } c= QC-symbols A

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { t where t is QC-symbol of A : s < t } or a in QC-symbols A )
assume a in { t where t is QC-symbol of A : s < t } ; :: thesis: a in QC-symbols A
then consider t being QC-symbol of A such that
A2: ( a = t & s < t ) ;
thus a in QC-symbols A by A2; :: thesis: verum

end;

ex a being set st a in { t where t is QC-symbol of A : s < t }

proof

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

suppose A3: s in NAT ; :: thesis: ex a being set st a in { t where t is QC-symbol of A : s < t }

then consider n being Nat such that
A4: s = n ;
reconsider a = n + 1 as Nat ;
NAT c= QC-symbols A by Th3;
then reconsider b = a as QC-symbol of A ;
( not n = a & n <= a ) by NAT_1:19;
then ( s <= b & not s = b ) by A4, Def33, A3;
then s < b ;
then b in { t where t is QC-symbol of A : s < t } ;
hence ex a being set st a in { t where t is QC-symbol of A : s < t } ; :: thesis: verum

end;

suppose A5: not s in NAT ; :: thesis: ex a being set st a in { t where t is QC-symbol of A : s < t }

reconsider a = 0 as QC-symbol of A by Th3;
( not s = a & s <= a ) by A5, Def33;
then s < a ;
then a in { t where t is QC-symbol of A : s < t } ;
hence ex a being set st a in { t where t is QC-symbol of A : s < t } ; :: thesis: verum

end;

end;

end;

hence { t where t is QC-symbol of A : s < t } is non empty Subset of (QC-symbols A) by A1; :: thesis: verum