let R be RelStr ; 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; 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); ( 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
; ( 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
; 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; verum