let R be RelStr ; :: thesis: for x, y being Element of R
for a, b being Element of (ComplRelStr R) st x = a & y = b & x <> y & x in the carrier of R & not a <= b holds
x <= y
let x, y be Element of R; :: thesis: for a, b being Element of (ComplRelStr R) st x = a & y = b & x <> y & x in the carrier of R & not a <= b holds
x <= y
let a, b be Element of (ComplRelStr R); :: thesis: ( x = a & y = b & x <> y & x in the carrier of R & not a <= b implies x <= y )
assume that
A: x = a and
B: y = b and
C: x <> y and
Ca: x in the carrier of R ; :: thesis: ( a <= b or x <= y )
set cR = the carrier of R;
set iR = the InternalRel of R;
set CR = ComplRelStr R;
set iCR = the InternalRel of (ComplRelStr R);
D: the InternalRel of (ComplRelStr R) = ( the InternalRel of R `) \ (id the carrier of R) by NECKLACE:def 9;
F: [x,y] in [: the carrier of R, the carrier of R:] by Ca, ZFMISC_1:def 2;
assume not a <= b ; :: thesis: x <= y
then A1: not [x,y] in the InternalRel of (ComplRelStr R) by A, B, ORDERS_2:def 9;
not [x,y] in id the carrier of R by C, RELAT_1:def 10;
then not [x,y] in the InternalRel of R ` by D, A1, XBOOLE_0:def 5;
then [x,y] in the InternalRel of R by F, XBOOLE_0:def 5;
hence x <= y by ORDERS_2:def 9; :: thesis: verum