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 that

A1: A,B form_upper_lower_partition_of L and

A2: A meets B ; :: thesis: contradiction

consider x being object such that

A3: x in A /\ B by A2, XBOOLE_0:4;

A4: x in B by A3, XBOOLE_0:def 4;

A5: x in A by A3, XBOOLE_0:def 4;

A \/ B = the carrier of L by A1;

then reconsider x = x as Element of L by A5, XBOOLE_0:def 3;

x < x by A1, A5, A4;

hence contradiction ; :: thesis: verum

A misses B

let A, B be set ; :: thesis: ( A,B form_upper_lower_partition_of L implies A misses B )

assume that

A1: A,B form_upper_lower_partition_of L and

A2: A meets B ; :: thesis: contradiction

consider x being object such that

A3: x in A /\ B by A2, XBOOLE_0:4;

A4: x in B by A3, XBOOLE_0:def 4;

A5: x in A by A3, XBOOLE_0:def 4;

A \/ B = the carrier of L by A1;

then reconsider x = x as Element of L by A5, XBOOLE_0:def 3;

x < x by A1, A5, A4;

hence contradiction ; :: thesis: verum