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 R9 = RelIncl {{a}};
reconsider R = RelIncl {{a}} as Relation of {{a}} ;
set L = RelStr(# {{a}},R #);
A1: RelStr(# {{a}},R #) is with_superior

proof

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

proof

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

end;

[max9,max9] in R by WELLORD2:def 1;
then max9 in field R by RELAT_1:15;
hence max9 is_superior_of the InternalRel of RelStr(# {{a}},R #) by A2, ORDERS_1:def 14; :: thesis: verum

end;

A5: 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 )
A6: y = {a} by TARSKI:def 1;
x = {a} by TARSKI:def 1;
then [x,y] in R by A6, WELLORD2:def 1;
hence ( x <= y or y <= x ) by ORDERS_2:def 5; :: thesis: verum

end;

RelStr(# {{a}},R #) = InclPoset {{a}} by YELLOW_1:def 1;
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, A5; :: thesis: verum