%% Clause labels found in directory Q:\glb
% GLB-CO-1
equal(GLB(composite(Id,x)),GLB(x)).
% DEF-GLB
equal(intersection(LB(x),complement(composite(complement(x),LB(x)))),GLB(x)).
% DEF-GLB
equal(intersection(complement(composite(complement(x),LB(x))),LB(x)),GLB(x)).
% I-2
equal(intersection(x,y),intersection(y,x)).
% GLB-V
subclass(GLB(x),cart(V,V)).
% GLB-FU-1
subclass(composite(GLB(x),inverse(GLB(x))),x).