let V be Universe; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 A1: ( X is closed_wrt_A1-A7 & A in X & B in X ) ; :: thesis: ( A \/ B in X & A \ B in X & A (#) B in X )
then reconsider a = A as Element of V ;
reconsider b = B as Element of V by A1;
A2: ( {a} in X & {b} in X ) by A1, Th2;
A3: X is closed_wrt_A5 by A1, Def13;
A4: X is closed_wrt_A6 by A1, Def13;
A5: X is closed_wrt_A7 by A1, Def13;
set D = { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } ;
A6: { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } in X by A2, A3, Def10;

now

let o be set ; :: thesis: ( o in { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a \/ b )

A7: now

assume o in { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } ; :: thesis: o = a \/ b
then consider x, y being Element of V such that
A8: ( o = x \/ y & x in {a} & y in {b} ) ;
( x = a & y = b ) by A8, TARSKI:def 1;
hence o = a \/ b by A8; :: thesis: verum

end;

now

assume A9: o = a \/ b ; :: thesis: o in { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) }
( a in {a} & b in {b} ) by TARSKI:def 1;
hence o in { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } by A9; :: thesis: verum

end;

hence ( o in { (x \/ y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a \/ b ) by A7; :: thesis: verum

end;

then {(a \/ b)} in X by A6, TARSKI:def 1;
hence A \/ B in X by A1, Th2; :: thesis: ( 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} ) } ;
A10: { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } in X by A2, A4, Def11;

now

let o be set ; :: thesis: ( o in { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a \ b )

A11: now

assume o in { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } ; :: thesis: o = a \ b
then consider x, y being Element of V such that
A12: ( o = x \ y & x in {a} & y in {b} ) ;
( x = a & y = b ) by A12, TARSKI:def 1;
hence o = a \ b by A12; :: thesis: verum

end;

now

assume A13: o = a \ b ; :: thesis: o in { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) }
( a in {a} & b in {b} ) by TARSKI:def 1;
hence o in { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } by A13; :: thesis: verum

end;

hence ( o in { (x \ y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a \ b ) by A11; :: thesis: verum

end;

then {(a \ b)} in X by A10, TARSKI:def 1;
hence A \ B in X by A1, Th2; :: thesis: A (#) B in X
set D = { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } ;
A14: { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } in X by A2, A5, Def12;

now

let o be set ; :: thesis: ( o in { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a (#) b )

A15: now

assume o in { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } ; :: thesis: o = a (#) b
then consider x, y being Element of V such that
A16: ( o = x (#) y & x in {a} & y in {b} ) ;
( x = a & y = b ) by A16, TARSKI:def 1;
hence o = a (#) b by A16; :: thesis: verum

end;

now

assume A17: o = a (#) b ; :: thesis: o in { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) }
( a in {a} & b in {b} ) by TARSKI:def 1;
hence o in { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } by A17; :: thesis: verum

end;

hence ( o in { (x (#) y) where x, y is Element of V : ( x in {a} & y in {b} ) } iff o = a (#) b ) by A15; :: thesis: verum

end;

then {(a (#) b)} in X by A14, TARSKI:def 1;
hence A (#) B in X by A1, Th2; :: thesis: verum