let X be non empty set ; :: thesis: for cB being empty Subset-Family of [:X,X:] holds not cB is axiom_UP1
let cB be empty Subset-Family of [:X,X:]; :: thesis: not cB is axiom_UP1
assume A1: cB is axiom_UP1 ; :: thesis: contradiction
{} is Element of cB by SUBSET_1:def 1;
then id X c= {} by A1;
hence contradiction ; :: thesis: verum