let n be Nat; for R being NatRelStr of n
for S being Subset of (Mycielskian R) st S = n holds
R = subrelstr S
let R be NatRelStr of n; for S being Subset of (Mycielskian R) st S = n holds
R = subrelstr S
let S be Subset of (Mycielskian R); ( S = n implies R = subrelstr S )
assume A1:
S = n
; R = subrelstr S
set cR = the carrier of R;
set iR = the InternalRel of R;
set sS = subrelstr S;
set csS = the carrier of (subrelstr S);
set isS = the InternalRel of (subrelstr S);
set MR = Mycielskian R;
set cMR = the carrier of (Mycielskian R);
set iMR = the InternalRel of (Mycielskian R);
A2:
the carrier of R = n
by Def7;
A3:
the carrier of (subrelstr S) = n
by A1, YELLOW_0:def 15;
A4:
the InternalRel of R = the InternalRel of (subrelstr S)
proof
thus
the
InternalRel of
R c= the
InternalRel of
(subrelstr S)
XBOOLE_0:def 10 the InternalRel of (subrelstr S) c= the InternalRel of Rproof
let z be
object ;
TARSKI:def 3 ( not z in the InternalRel of R or z in the InternalRel of (subrelstr S) )
assume A5:
z in the
InternalRel of
R
;
z in the InternalRel of (subrelstr S)
then consider x,
y being
object such that A6:
x in the
carrier of
R
and A7:
y in the
carrier of
R
and A8:
z = [x,y]
by ZFMISC_1:def 2;
the
carrier of
R c= the
carrier of
(Mycielskian R)
by Th37;
then reconsider xMR =
x,
yMR =
y as
Element of
(Mycielskian R) by A6, A7;
reconsider xsS =
x,
ysS =
y as
Element of
(subrelstr S) by A6, A7, Def7, A3;
the
InternalRel of
R c= the
InternalRel of
(Mycielskian R)
by Th39;
then
xMR <= yMR
by A5, A8, ORDERS_2:def 5;
then
xsS <= ysS
by A3, A2, A7, YELLOW_0:60;
hence
z in the
InternalRel of
(subrelstr S)
by A8, ORDERS_2:def 5;
verum
end;
thus
the
InternalRel of
(subrelstr S) c= the
InternalRel of
R
verumproof
let z be
object ;
TARSKI:def 3 ( not z in the InternalRel of (subrelstr S) or z in the InternalRel of R )
assume A9:
z in the
InternalRel of
(subrelstr S)
;
z in the InternalRel of R
then consider x,
y being
object such that A10:
x in Segm n
and A11:
y in Segm n
and A12:
z = [x,y]
by ZFMISC_1:def 2, A3;
the
carrier of
R c= the
carrier of
(Mycielskian R)
by Th37;
then reconsider xMR =
x,
yMR =
y as
Element of
(Mycielskian R) by A10, A11, A2;
reconsider xsS =
x,
ysS =
y as
Element of
(subrelstr S) by A10, A11, A3;
xsS <= ysS
by A9, A12, ORDERS_2:def 5;
then
xMR <= yMR
by YELLOW_0:59;
then
z in the
InternalRel of
(Mycielskian R)
by A12, ORDERS_2:def 5;
hence
z in the
InternalRel of
R
by A10, A11, A12, Th40;
verum
end;
end;
thus
R = subrelstr S
by Def7, A3, A4; verum