let L be RelStr ; for A, B being set st A,B form_upper_lower_partition_of L holds
A misses B
let A, B be set ; ( 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
; 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
; verum