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 A:
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);
B:
the carrier of R = n
by LNRS;
Ba:
the carrier of (subrelstr S) = n
by A, YELLOW_0:def 15;
C:
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
set ;
TARSKI:def 3 ( not z in the InternalRel of R or z in the InternalRel of (subrelstr S) )
assume A0:
z in the
InternalRel of
R
;
z in the InternalRel of (subrelstr S)
then consider x,
y being
set such that A1:
x in the
carrier of
R
and B1:
y in the
carrier of
R
and C1:
z = [x,y]
by ZFMISC_1:def 2;
the
carrier of
R c= the
carrier of
(Mycielskian R)
by cMR0;
then reconsider xMR =
x,
yMR =
y as
Element of
(Mycielskian R) by A1, B1;
reconsider xsS =
x,
ysS =
y as
Element of
(subrelstr S) by A1, B1, LNRS, Ba;
the
InternalRel of
R c= the
InternalRel of
(Mycielskian R)
by iMR1ba;
then
xMR <= yMR
by A0, C1, ORDERS_2:def 9;
then
xsS <= ysS
by Ba, B, B1, YELLOW_0:61;
hence
z in the
InternalRel of
(subrelstr S)
by C1, ORDERS_2:def 9;
verum
end;
thus
the
InternalRel of
(subrelstr S) c= the
InternalRel of
R
verumproof
let z be
set ;
TARSKI:def 3 ( not z in the InternalRel of (subrelstr S) or z in the InternalRel of R )
assume A0:
z in the
InternalRel of
(subrelstr S)
;
z in the InternalRel of R
then consider x,
y being
set such that A1:
x in the
carrier of
(subrelstr S)
and B1:
y in the
carrier of
(subrelstr S)
and C1:
z = [x,y]
by ZFMISC_1:def 2;
the
carrier of
R c= the
carrier of
(Mycielskian R)
by cMR0;
then reconsider xMR =
x,
yMR =
y as
Element of
(Mycielskian R) by A1, B1, B, Ba;
reconsider xsS =
x,
ysS =
y as
Element of
(subrelstr S) by A1, B1;
xsS <= ysS
by A0, C1, ORDERS_2:def 9;
then
xMR <= yMR
by YELLOW_0:60;
then
z in the
InternalRel of
(Mycielskian R)
by C1, ORDERS_2:def 9;
hence
z in the
InternalRel of
R
by A1, B1, Ba, C1, iMR1b;
verum
end;
end;
thus
R = subrelstr S
by LNRS, Ba, C; verum