let S be RelStr ; :: thesis: ( S is flat implies ( S is reflexive & S is transitive & S is antisymmetric ) )
assume S is flat ; :: thesis: ( 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

proof

for x being object st x in the carrier of S holds
[x,x] in the InternalRel of S

proof

let x be object ; :: thesis: ( x in the carrier of S implies [x,x] in the InternalRel of S )
assume x in the carrier of S ; :: thesis: [x,x] in the InternalRel of S
then reconsider x = x as Element of S ;
x <= x by A1;
hence [x,x] in the InternalRel of S ; :: thesis: verum

end;

hence the InternalRel of S is_reflexive_in the carrier of S ; :: thesis: verum

end;

hence S is reflexive ; :: thesis: ( 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 ; :: thesis: ( 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 ) ; :: thesis: [x,z] in the InternalRel of S
then reconsider x = x, y = y, z = z as Element of S ;
x <= z

proof

( x = a or x = y ) by B1, ORDERS_2:def 5, A1;
hence x <= z by A1, B1; :: thesis: verum

end;

hence [x,z] in the InternalRel of S ; :: thesis: verum

end;

hence the InternalRel of S is_transitive_in the carrier of S ; :: thesis: verum

end;

hence S is transitive ; :: thesis: 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 ; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum

end;

hence the InternalRel of S is_antisymmetric_in the carrier of S ; :: thesis: verum

end;

hence S is antisymmetric ; :: thesis: verum