set T = dom B;
set S = { p where p is Element of J : not p is dom B -headed } ;
for a being object st a in { p where p is Element of J : not p is dom B -headed } holds
a in J

proof

let a be object ; :: thesis: ( a in { p where p is Element of J : not p is dom B -headed } implies a in J )
assume a in { p where p is Element of J : not p is dom B -headed } ; :: thesis: a in J
then consider p being Element of J such that
A1: a = p and
not p is dom B -headed ;
thus a in J by A1; :: thesis: verum

end;

then { p where p is Element of J : not p is dom B -headed } c= J ;
hence { p where p is Element of J : not p is dom B -headed } is Subset of J ; :: thesis: verum