( sqrt (DC p) in {(sqrt (DC p))} & {(sqrt (DC p))} is Subset of (FAdj (F,{(sqrt (DC p))})) ) by TARSKI:def 1, FIELD_6:35;
hence sqrt (DC p) is Element of (FAdj (F,{(sqrt (DC p))})) ; :: thesis: verum