let X be set ; :: thesis: for F being Field_Subset of X holds X in F
let F be Field_Subset of X; :: thesis: X in F
consider A being Subset of X such that
A1: A in F by SUBSET_1:4;
A2: A \/ (A `) = [#] X by SUBSET_1:10
.= X ;
A ` in F by A1, Def1;
hence X in F by A1, A2, Th3; :: thesis: verum