let S be RelStr ; ( S is flat implies ( S is reflexive & S is transitive & S is antisymmetric ) )
assume
S is flat
; ( S is reflexive & S is transitive & S is antisymmetric )
then consider a being Element of S such that
A1:
for x, y being Element of S holds
( x <= y iff ( x = a or x = y ) )
;
set R = the InternalRel of S;
set X = the carrier of S;
the InternalRel of S is_reflexive_in the carrier of S
hence
S is reflexive
; ( S is transitive & S is antisymmetric )
the InternalRel of S is_transitive_in the carrier of S
proof
for
x,
y,
z being
object st
x in the
carrier of
S &
y in the
carrier of
S &
z in the
carrier of
S &
[x,y] in the
InternalRel of
S &
[y,z] in the
InternalRel of
S holds
[x,z] in the
InternalRel of
S
proof
let x,
y,
z be
object ;
( x in the carrier of S & y in the carrier of S & z in the carrier of S & [x,y] in the InternalRel of S & [y,z] in the InternalRel of S implies [x,z] in the InternalRel of S )
assume B1:
(
x in the
carrier of
S &
y in the
carrier of
S &
z in the
carrier of
S &
[x,y] in the
InternalRel of
S &
[y,z] in the
InternalRel of
S )
;
[x,z] in the InternalRel of S
then reconsider x =
x,
y =
y,
z =
z as
Element of
S ;
x <= z
hence
[x,z] in the
InternalRel of
S
;
verum
end;
hence
the
InternalRel of
S is_transitive_in the
carrier of
S
;
verum
end;
hence
S is transitive
; S is antisymmetric
the InternalRel of S is_antisymmetric_in the carrier of S
proof
for
x,
y being
object st
x in the
carrier of
S &
y in the
carrier of
S &
[x,y] in the
InternalRel of
S &
[y,x] in the
InternalRel of
S holds
x = y
proof
let x,
y be
object ;
( x in the carrier of S & y in the carrier of S & [x,y] in the InternalRel of S & [y,x] in the InternalRel of S implies x = y )
assume B1:
(
x in the
carrier of
S &
y in the
carrier of
S &
[x,y] in the
InternalRel of
S &
[y,x] in the
InternalRel of
S )
;
x = y
then reconsider x =
x,
y =
y as
Element of
S ;
(
x = a or
x = y )
by B1, ORDERS_2:def 5, A1;
hence
x = y
by A1, B1, ORDERS_2:def 5;
verum
end;
hence
the
InternalRel of
S is_antisymmetric_in the
carrier of
S
;
verum
end;
hence
S is antisymmetric
; verum