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
A1: x = a and
A2: y = b and
A3: x <> y and
A4: 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);
A5: the InternalRel of (ComplRelStr R) = ( the InternalRel of R `) \ (id the carrier of R) by NECKLACE:def 8;
A6: [x,y] in [: the carrier of R, the carrier of R:] by A4, ZFMISC_1:def 2;
assume not a <= b ; :: thesis: x <= y
then A7: not [x,y] in the InternalRel of (ComplRelStr R) by A1, A2, ORDERS_2:def 5;
not [x,y] in id the carrier of R by A3, RELAT_1:def 10;
then not [x,y] in the InternalRel of R ` by A5, A7, XBOOLE_0:def 5;
then [x,y] in the InternalRel of R by A6, XBOOLE_0:def 5;
hence x <= y by ORDERS_2:def 5; :: thesis: verum