let L be non empty antisymmetric upper-bounded RelStr ; :: thesis: the carrier of L \ {(Top L)},{(Top L)} form_upper_lower_partition_of L
A1: (the carrier of L \ {(Top L)}) \/ {(Top L)} = the carrier of L by XBOOLE_1:45;
for a, b being Element of L st a in the carrier of L \ {(Top L)} & b in {(Top L)} holds
a < b

proof

let a, b be Element of L; :: thesis: ( a in the carrier of L \ {(Top L)} & b in {(Top L)} implies a < b )
assume A2: ( a in the carrier of L \ {(Top L)} & b in {(Top L)} ) ; :: thesis: a < b
then ( a in the carrier of L & not a in {(Top L)} ) by XBOOLE_0:def 5;
then A3: ( a in the carrier of L & a <> Top L ) by TARSKI:def 1;
A4: b = Top L by A2, TARSKI:def 1;
a <= Top L by YELLOW_0:45;
hence a < b by A3, A4, ORDERS_2:def 10; :: thesis: verum

end;

hence the carrier of L \ {(Top L)},{(Top L)} form_upper_lower_partition_of L by A1, Def3; :: thesis: verum