environ
vocabularies HIDDEN, XBOOLE_0, SUBSET_1, TARSKI, ORDERS_2, WAYBEL_0, XXREAL_0, ZFMISC_1, RELAT_1, MCART_1, LATTICE3, RELAT_2, LATTICES, YELLOW_0, EQREL_1, REWRITE1, ORDINAL2, FUNCT_1, STRUCT_0, YELLOW_3;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, RELAT_2, RELSET_1, MCART_1, DOMAIN_1, FUNCT_2, BINOP_1, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0;
definitions LATTICE3, RELAT_2, TARSKI, WAYBEL_0, ORDERS_2;
theorems FUNCT_1, FUNCT_2, FUNCT_5, LATTICE3, MCART_1, ORDERS_2, RELAT_1, RELAT_2, RELSET_1, TARSKI, WAYBEL_0, YELLOW_0, YELLOW_2, ZFMISC_1, XBOOLE_0, BINOP_1, XTUPLE_0;
schemes FUNCT_7, RELAT_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, LATTICE3, YELLOW_0, ORDERS_2, WAYBEL_0, RELAT_1, XTUPLE_0;
constructors HIDDEN, DOMAIN_1, LATTICE3, ORDERS_3, WAYBEL_0, RELSET_1, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities ;
expansions LATTICE3, RELAT_2, WAYBEL_0, ORDERS_2;
scheme
FraenkelA2{
F1()
-> non
empty set ,
F2(
set ,
set )
-> set ,
P1[
set ,
set ],
P2[
set ,
set ] } :
{ F2(s,t) where s, t is Element of F1() : P1[s,t] } is
Subset of
F1()
provided
A1:
for
s,
t being
Element of
F1() holds
F2(
s,
t)
in F1()
definition
let P,
R be
Relation;
func ["P,R"] -> Relation means :
Def1:
for
x,
y being
object holds
(
[x,y] in it iff ex
p,
q,
s,
t being
object st
(
x = [p,q] &
y = [s,t] &
[p,s] in P &
[q,t] in R ) );
existence
ex b1 being Relation st
for x, y being object holds
( [x,y] in b1 iff ex p, q, s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) )
uniqueness
for b1, b2 being Relation st ( for x, y being object holds
( [x,y] in b1 iff ex p, q, s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) & ( for x, y being object holds
( [x,y] in b2 iff ex p, q, s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) holds
b1 = b2
end;
::
deftheorem Def1 defines
[" YELLOW_3:def 1 :
for P, R, b3 being Relation holds
( b3 = ["P,R"] iff for x, y being object holds
( [x,y] in b3 iff ex p, q, s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) );
theorem Th10:
for
P,
R being
Relation for
x being
object holds
(
x in ["P,R"] iff (
[((x `1) `1),((x `2) `1)] in P &
[((x `1) `2),((x `2) `2)] in R & ex
a,
b being
object st
x = [a,b] & ex
c,
d being
object st
x `1 = [c,d] & ex
e,
f being
object st
x `2 = [e,f] ) )
definition
let A,
B,
X,
Y be
set ;
let P be
Relation of
A,
B;
let R be
Relation of
X,
Y;
["redefine func ["P,R"] -> Relation of
[:A,X:],
[:B,Y:];
coherence
["P,R"] is Relation of [:A,X:],[:B,Y:]
end;