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 Th6;
A2: A ` in F by A1, Def1;
A \/ (A ` ) = [#] X by SUBSET_1:25
.= X ;
hence X in F by A1, A2, Th9; :: thesis: verum