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

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

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

( the carrier of L \ {(Top L)}) \/ {(Top L)} = the carrier of L
by XBOOLE_1:45;
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;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

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