let X be set ; :: thesis: for F being Field_Subset of X holds
( {{} ,X} c= F & F c= bool X )
let F be Field_Subset of X; :: thesis: ( {{} ,X} c= F & F c= bool X )
A1: {} in F by Th10;
X in F by Th11;
then for x being set st x in {{} ,X} holds
x in F by A1, TARSKI:def 2;
hence ( {{} ,X} c= F & F c= bool X ) by TARSKI:def 3; :: thesis: verum