let V be Universe; :: thesis: for X being Subclass of V
for o, A being set st X is closed_wrt_A1-A7 holds
( ( o in X implies {o} in X ) & ( {o} in X implies o in X ) & ( A in X implies union A in X ) )
let X be Subclass of V; :: thesis: for o, A being set st X is closed_wrt_A1-A7 holds
( ( o in X implies {o} in X ) & ( {o} in X implies o in X ) & ( A in X implies union A in X ) )
let o, A be set ; :: thesis: ( X is closed_wrt_A1-A7 implies ( ( o in X implies {o} in X ) & ( {o} in X implies o in X ) & ( A in X implies union A in X ) ) )
assume A1: X is closed_wrt_A1-A7 ; :: thesis: ( ( o in X implies {o} in X ) & ( {o} in X implies o in X ) & ( A in X implies union A in X ) )
then A2: X is closed_wrt_A2 ;
A3: now :: thesis: ( o in X implies {o} in X )
assume o in X ; :: thesis: {o} in X
then {o,o} in X by A2;
hence {o} in X by ENUMSET1:29; :: thesis: verum
end;
A4: X is closed_wrt_A3 by A1;
now :: thesis: ( {o} in X implies o in X )
assume {o} in X ; :: thesis: o in X
then union {o} in X by A4;
hence o in X by ZFMISC_1:25; :: thesis: verum
end;
hence ( o in X iff {o} in X ) by A3; :: thesis: ( A in X implies union A in X )
assume A in X ; :: thesis: union A in X
hence union A in X by A4; :: thesis: verum