per cases ( the entourages of USS is empty or not the entourages of USS is empty ) ;
suppose the entourages of USS is empty ; :: thesis: V1 /\ V2 is Element of the entourages of USS
then ( V1 = {} & V2 = {} ) by SUBSET_1:def 1;
hence V1 /\ V2 is Element of the entourages of USS ; :: thesis: verum
end;
suppose A1: not the entourages of USS is empty ; :: thesis: V1 /\ V2 is Element of the entourages of USS
USS is cap-closed ;
hence V1 /\ V2 is Element of the entourages of USS by A1, FINSUB_1:def 2; :: thesis: verum
end;
end;