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

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