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 set 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, Def3;
then reconsider x = x as Element of L by A5, XBOOLE_0:def 3;
x < x by A1, A5, A4, Def3;
hence contradiction ; :: thesis: verum