let A be QC-alphabet ; :: thesis: for Y1, Y2 being non empty Subset of (QC-symbols A) st Y1 c= Y2 holds
min Y2 <= min Y1
let Y1, Y2 be non empty Subset of (QC-symbols A); :: thesis: ( Y1 c= Y2 implies min Y2 <= min Y1 )
assume A1: Y1 c= Y2 ; :: thesis: min Y2 <= min Y1
min Y1 in Y1 by Def35;
hence min Y2 <= min Y1 by A1, Def35; :: thesis: verum