let V be Universe; for X being Subclass of V
for A, B being set st X is closed_wrt_A1-A7 & A in X & B in X holds
( A \/ B in X & A \ B in X & A (#) B in X )
let X be Subclass of V; for A, B being set st X is closed_wrt_A1-A7 & A in X & B in X holds
( A \/ B in X & A \ B in X & A (#) B in X )
let A, B be set ; ( X is closed_wrt_A1-A7 & A in X & B in X implies ( A \/ B in X & A \ B in X & A (#) B in X ) )
assume that
A1:
X is closed_wrt_A1-A7
and
A2:
A in X
and
A3:
B in X
; ( A \/ B in X & A \ B in X & A (#) B in X )
reconsider b = B as Element of V by A3;
reconsider a = A as Element of V by A2;
A4:
( {a} in X & {b} in X )
by A1, A2, A3, Th2;
set D = { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } ;
X is closed_wrt_A5
by A1;
then
{ (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } in X
by A4;
then
{(a \/ b)} in X
by A5, TARSKI:def 1;
hence
A \/ B in X
by A1, Th2; ( A \ B in X & A (#) B in X )
set D = { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } ;
X is closed_wrt_A6
by A1;
then
{ (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } in X
by A4;
then
{(a \ b)} in X
by A11, TARSKI:def 1;
hence
A \ B in X
by A1, Th2; A (#) B in X
set D = { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } ;
X is closed_wrt_A7
by A1;
then
{ (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } in X
by A4;
then
{(a (#) b)} in X
by A17, TARSKI:def 1;
hence
A (#) B in X
by A1, Th2; verum