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