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: 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 that
A2: a in the carrier of L \ {(Top L)} and
A3: b in {(Top L)} ; :: thesis: a < b
not a in {(Top L)} by A2, XBOOLE_0:def 5;
then A4: a <> Top L by TARSKI:def 1;
A5: a <= Top L by YELLOW_0:45;
b = Top L by A3, TARSKI:def 1;
hence a < b by A4, A5, ORDERS_2:def 6; :: thesis: verum
end;
( the carrier of L \ {(Top L)}) \/ {(Top L)} = the carrier of L by XBOOLE_1:45;
hence the carrier of L \ {(Top L)},{(Top L)} form_upper_lower_partition_of L by A1; :: thesis: verum