let A, B be Ring; :: thesis: for a being Element of A st A is Subring of B holds
a is Element of B
let a be Element of A; :: thesis: ( A is Subring of B implies a is Element of B )
assume A is Subring of B ; :: thesis: a is Element of B
then the carrier of A c= the carrier of B by C0SP1:def 3;
hence a is Element of B ; :: thesis: verum