set AB = { (A \ B) where A, B is Element of S : verum } ;
{ (A \ B) where A, B is Element of S : verum } c= bool X
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { (A \ B) where A, B is Element of S : verum } or t in bool X )
assume t in { (A \ B) where A, B is Element of S : verum } ; :: thesis: t in bool X
then consider A0, B0 being Element of S such that
A1: t = A0 \ B0 ;
thus t in bool X by A1; :: thesis: verum
end;
then reconsider AB = { (A \ B) where A, B is Element of S : verum } as Subset-Family of X ;
{} in S by SETFAM_1:def 8;
then {} \ {} in AB ;
hence DIFFERENCE (S,S) is Subset-Family of X by LemY; :: thesis: verum