let V be Universe; :: thesis: for X being Subclass of V
for o, p being set st X is closed_wrt_A1-A7 & o in X & p in X holds
( {o,p} in X & [o,p] in X )
let X be Subclass of V; :: thesis: for o, p being set st X is closed_wrt_A1-A7 & o in X & p in X holds
( {o,p} in X & [o,p] in X )
let o, p be set ; :: thesis: ( X is closed_wrt_A1-A7 & o in X & p in X implies ( {o,p} in X & [o,p] in X ) )
assume that
A1: X is closed_wrt_A1-A7 and
A2: o in X and
A3: p in X ; :: thesis: ( {o,p} in X & [o,p] in X )
reconsider a = o, b = p as Element of V by A2, A3;
A4: {o} in X by A1, A2, Th2;
A5: X is closed_wrt_A2 by A1;
hence {o,p} in X by A2, A3; :: thesis: [o,p] in X
{a,b} in X by A2, A3, A5;
hence [o,p] in X by A5, A4; :: thesis: verum