set E = InducedSubfield S;
A: the carrier of (InducedSubfield S) = S by dis;
then ( the carrier of (InducedSubfield S) c= the carrier of F & the addF of (InducedSubfield S) = the addF of F || S & the multF of (InducedSubfield S) = the multF of F || S & 0. (InducedSubfield S) = 0. F & 1. (InducedSubfield S) = 1. F ) by dis;
hence InducedSubfield S is strict Subfield of F by A, EC_PF_1:def 1; :: thesis: verum