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 holds
not a <= b
let x, y be Element of R; :: thesis: for a, b being Element of (ComplRelStr R) st x = a & y = b & x <= y holds
not a <= b
let a, b be Element of (ComplRelStr R); :: thesis: ( x = a & y = b & x <= y implies not a <= b )
assume that
A1: x = a and
A2: y = b ; :: thesis: ( not x <= y or not a <= b )
set cR = the carrier of R;
set iR = the InternalRel of R;
set CR = ComplRelStr R;
set iCR = the InternalRel of (ComplRelStr R);
A3: the InternalRel of (ComplRelStr R) = ( the InternalRel of R `) \ (id the carrier of R) by NECKLACE:def 8;
assume x <= y ; :: thesis: not a <= b
then [x,y] in the InternalRel of R by ORDERS_2:def 5;
then not [x,y] in the InternalRel of R ` by XBOOLE_0:def 5;
then not [x,y] in the InternalRel of (ComplRelStr R) by A3, XBOOLE_0:def 5;
hence not a <= b by A1, A2, ORDERS_2:def 5; :: thesis: verum