let R be Field; :: thesis: for S being FieldExtension of R
for T being Subset of S
for x being Element of (FAdj (R,T)) holds x is Element of S
let S be FieldExtension of R; :: thesis: for T being Subset of S
for x being Element of (FAdj (R,T)) holds x is Element of S
let T be Subset of S; :: thesis: for x being Element of (FAdj (R,T)) holds x is Element of S
let x be Element of (FAdj (R,T)); :: thesis: x is Element of S
A1: the carrier of (FAdj (R,T)) = carrierFA T by dFA;
x in the carrier of (FAdj (R,T)) ;
hence x is Element of S by A1; :: thesis: verum