let L be RelStr ; :: thesis: for A, B being set st A,B form_upper_lower_partition_of L holds
A misses B
let A, B be set ; :: thesis: ( A,B form_upper_lower_partition_of L implies A misses B )
assume A1: ( A,B form_upper_lower_partition_of L & A meets B ) ; :: thesis: contradiction
then A2: ( A \/ B = the carrier of L & ( for a, b being Element of L st a in A & b in B holds
a < b ) ) by Def3;
consider x being set such that
A3: x in A /\ B by A1, XBOOLE_0:4;
A4: ( x in A & x in B ) by A3, XBOOLE_0:def 4;
then reconsider x = x as Element of L by A2, XBOOLE_0:def 3;
x < x by A1, A4, Def3;
hence contradiction ; :: thesis: verum