begin
definition
let X1,
X2,
X3 be non
empty set ;
let x1 be
Element of
X1;
let x2 be
Element of
X2;
let x3 be
Element of
X3;
[redefine func [x1,x2,x3] -> Element of
[:X1,X2,X3:];
coherence
[x1,x2,x3] is Element of [:X1,X2,X3:]
by MCART_1:69;
end;
theorem Th11:
for
D,
X1,
X2,
X3,
X4 being non
empty set st ( for
a being
set holds
(
a in D iff ex
x1 being
Element of
X1 ex
x2 being
Element of
X2 ex
x3 being
Element of
X3 ex
x4 being
Element of
X4 st
a = [x1,x2,x3,x4] ) ) holds
D = [:X1,X2,X3,X4:]
theorem
for
D,
X1,
X2,
X3,
X4 being non
empty set holds
(
D = [:X1,X2,X3,X4:] iff for
a being
set holds
(
a in D iff ex
x1 being
Element of
X1 ex
x2 being
Element of
X2 ex
x3 being
Element of
X3 ex
x4 being
Element of
X4 st
a = [x1,x2,x3,x4] ) )
by Th10, Th11;
definition
let X1,
X2,
X3,
X4 be non
empty set ;
let x1 be
Element of
X1;
let x2 be
Element of
X2;
let x3 be
Element of
X3;
let x4 be
Element of
X4;
[redefine func [x1,x2,x3,x4] -> Element of
[:X1,X2,X3,X4:];
coherence
[x1,x2,x3,x4] is Element of [:X1,X2,X3,X4:]
by MCART_1:80;
end;
scheme
Fraenkel3{
P1[
set ,
set ,
set ] } :
for
X1,
X2,
X3 being non
empty set holds
{ [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P1[x1,x2,x3] } is
Subset of
[:X1,X2,X3:]
scheme
Fraenkel4{
P1[
set ,
set ,
set ,
set ] } :
for
X1,
X2,
X3,
X4 being non
empty set holds
{ [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : P1[x1,x2,x3,x4] } is
Subset of
[:X1,X2,X3,X4:]
scheme
Fraenkel5{
P1[
set ],
P2[
set ] } :
for
X1 being non
empty set st ( for
x1 being
Element of
X1 st
P1[
x1] holds
P2[
x1] ) holds
{ y1 where y1 is Element of X1 : P1[y1] } c= { z1 where z1 is Element of X1 : P2[z1] }
scheme
Fraenkel6{
P1[
set ],
P2[
set ] } :
for
X1 being non
empty set st ( for
x1 being
Element of
X1 holds
(
P1[
x1] iff
P2[
x1] ) ) holds
{ y1 where y1 is Element of X1 : P1[y1] } = { z1 where z1 is Element of X1 : P2[z1] }
theorem
for
X1,
X2,
X3,
X4 being non
empty set holds
[:X1,X2,X3,X4:] = { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum }
theorem
for
X1,
X2,
X3,
X4 being non
empty set for
A1 being
Subset of
X1 for
A2 being
Subset of
X2 for
A3 being
Subset of
X3 for
A4 being
Subset of
X4 holds
[:A1,A2,A3,A4:] = { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) }
theorem
for
X1 being non
empty set for
A1,
B1 being
Subset of
X1 holds
A1 \ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 ) }
theorem Th31:
for
X1 being non
empty set for
A1,
B1 being
Subset of
X1 holds
A1 \+\ B1 = { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) }
theorem
for
X1 being non
empty set for
A1,
B1 being
Subset of
X1 holds
A1 \+\ B1 = { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( x1 in B1 & not x1 in A1 ) ) }
definition
let D be non
empty set ;
let x1 be
Element of
D;
{redefine func {x1} -> Subset of
D;
coherence
{x1} is Subset of D
by SUBSET_1:33;
let x2 be
Element of
D;
{redefine func {x1,x2} -> Subset of
D;
coherence
{x1,x2} is Subset of D
by SUBSET_1:34;
let x3 be
Element of
D;
{redefine func {x1,x2,x3} -> Subset of
D;
coherence
{x1,x2,x3} is Subset of D
by SUBSET_1:35;
let x4 be
Element of
D;
{redefine func {x1,x2,x3,x4} -> Subset of
D;
coherence
{x1,x2,x3,x4} is Subset of D
by SUBSET_1:36;
let x5 be
Element of
D;
{redefine func {x1,x2,x3,x4,x5} -> Subset of
D;
coherence
{x1,x2,x3,x4,x5} is Subset of D
by SUBSET_1:37;
let x6 be
Element of
D;
{redefine func {x1,x2,x3,x4,x5,x6} -> Subset of
D;
coherence
{x1,x2,x3,x4,x5,x6} is Subset of D
by SUBSET_1:38;
let x7 be
Element of
D;
{redefine func {x1,x2,x3,x4,x5,x6,x7} -> Subset of
D;
coherence
{x1,x2,x3,x4,x5,x6,x7} is Subset of D
by SUBSET_1:39;
let x8 be
Element of
D;
{redefine func {x1,x2,x3,x4,x5,x6,x7,x8} -> Subset of
D;
coherence
{x1,x2,x3,x4,x5,x6,x7,x8} is Subset of D
by SUBSET_1:40;
end;
begin