let P, Q be pcs-Str ; :: thesis: for p being set st p in the carrier of P & P c= Q holds
p is Element of Q
let p be set ; :: thesis: ( p in the carrier of P & P c= Q implies p is Element of Q )
assume A1: p in the carrier of P ; :: thesis: ( not P c= Q or p is Element of Q )
assume P c= Q ; :: thesis: p is Element of Q
then the carrier of P c= the carrier of Q by Def34;
hence p is Element of Q by A1; :: thesis: verum