let a be set ; :: thesis: ( not InclPoset {{a}} is empty & InclPoset {{a}} is reflexive & InclPoset {{a}} is transitive & InclPoset {{a}} is antisymmetric & InclPoset {{a}} is with_superior & InclPoset {{a}} is with_comparable_down )
set A = {{a}};
set R' = RelIncl {{a}};
reconsider R = RelIncl {{a}} as Relation of {{a}} ;
A1: RelStr(# {{a}},R #) = InclPoset {{a}} by YELLOW_1:def 1;
set L = RelStr(# {{a}},R #);
A2: RelStr(# {{a}},R #) is with_superior

proof

set max = {a};
reconsider max' = {a} as Element of RelStr(# {{a}},R #) by TARSKI:def 1;
take max' ; :: according to TAXONOM2:def 1 :: thesis: max' is_superior_of the InternalRel of RelStr(# {{a}},R #)
[max',max'] in R by WELLORD2:def 1;
then A3: max' in field R by RELAT_1:30;
for y being set st y in field R & y <> max' holds
[y,max'] in R

proof

let y be set ; :: thesis: ( y in field R & y <> max' implies [y,max'] in R )
assume A4: ( y in field R & y <> max' ) ; :: thesis: [y,max'] in R
field R c= {{a}} \/ {{a}} by RELSET_1:19;
hence [y,max'] in R by A4, TARSKI:def 1; :: thesis: verum

end;

hence max' is_superior_of the InternalRel of RelStr(# {{a}},R #) by A3, ORDERS_1:def 13; :: thesis: verum

end;

for x, y being Element of RelStr(# {{a}},R #) holds
( for z being Element of RelStr(# {{a}},R #) holds
( not z <= x or not z <= y ) or x <= y or y <= x )

proof

let x, y be Element of RelStr(# {{a}},R #); :: thesis: ( for z being Element of RelStr(# {{a}},R #) holds
( not z <= x or not z <= y ) or x <= y or y <= x )
assume ex z being Element of RelStr(# {{a}},R #) st
( z <= x & z <= y ) ; :: thesis: ( x <= y or y <= x )
( x = {a} & y = {a} ) by TARSKI:def 1;
then [x,y] in R by WELLORD2:def 1;
hence ( x <= y or y <= x ) by ORDERS_2:def 9; :: thesis: verum

end;

hence ( not InclPoset {{a}} is empty & InclPoset {{a}} is reflexive & InclPoset {{a}} is transitive & InclPoset {{a}} is antisymmetric & InclPoset {{a}} is with_superior & InclPoset {{a}} is with_comparable_down ) by A1, A2, Def2; :: thesis: verum