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 )
( {} in F & X in F ) by Th10, Th11;
then for x being set st x in {{} ,X} holds
x in F by TARSKI:def 2;
hence ( {{} ,X} c= F & F c= bool X ) by TARSKI:def 3; :: thesis: verum