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

( {{},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