set R = Sub L;

thus Sub L is reflexive :: thesis: ( Sub L is antisymmetric & Sub L is transitive )

thus Sub L is reflexive :: thesis: ( Sub L is antisymmetric & Sub L is transitive )

proof

thus
Sub L is antisymmetric
:: thesis: Sub L is transitive
let x be Element of (Sub L); :: according to YELLOW_0:def 1 :: thesis: x <= x

reconsider A = x as strict SubRelStr of L by Def2;

A is SubRelStr of A by YELLOW_0:def 13;

hence x <= x by Th15; :: thesis: verum

end;reconsider A = x as strict SubRelStr of L by Def2;

A is SubRelStr of A by YELLOW_0:def 13;

hence x <= x by Th15; :: thesis: verum

proof

thus
Sub L is transitive
:: thesis: verum
let x, y be Element of (Sub L); :: according to YELLOW_0:def 3 :: thesis: ( not x <= y or not y <= x or x = y )

reconsider A = x, B = y as strict SubRelStr of L by Def2;

assume that

A1: x <= y and

A2: y <= x ; :: thesis: x = y

A3: B is SubRelStr of A by A2, Th15;

then A4: the carrier of B c= the carrier of A by YELLOW_0:def 13;

A5: A is SubRelStr of B by A1, Th15;

then the carrier of A c= the carrier of B by YELLOW_0:def 13;

then A6: the carrier of A = the carrier of B by A4;

A7: the InternalRel of B c= the InternalRel of A by A3, YELLOW_0:def 13;

the InternalRel of A c= the InternalRel of B by A5, YELLOW_0:def 13;

hence x = y by A7, A6, XBOOLE_0:def 10; :: thesis: verum

end;reconsider A = x, B = y as strict SubRelStr of L by Def2;

assume that

A1: x <= y and

A2: y <= x ; :: thesis: x = y

A3: B is SubRelStr of A by A2, Th15;

then A4: the carrier of B c= the carrier of A by YELLOW_0:def 13;

A5: A is SubRelStr of B by A1, Th15;

then the carrier of A c= the carrier of B by YELLOW_0:def 13;

then A6: the carrier of A = the carrier of B by A4;

A7: the InternalRel of B c= the InternalRel of A by A3, YELLOW_0:def 13;

the InternalRel of A c= the InternalRel of B by A5, YELLOW_0:def 13;

hence x = y by A7, A6, XBOOLE_0:def 10; :: thesis: verum

proof

let x, y, z be Element of (Sub L); :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )

reconsider A = x, B = y, C = z as strict SubRelStr of L by Def2;

assume that

A8: x <= y and

A9: y <= z ; :: thesis: x <= z

A10: B is SubRelStr of C by A9, Th15;

then A11: the carrier of B c= the carrier of C by YELLOW_0:def 13;

A12: the InternalRel of B c= the InternalRel of C by A10, YELLOW_0:def 13;

A13: A is SubRelStr of B by A8, Th15;

then the InternalRel of A c= the InternalRel of B by YELLOW_0:def 13;

then A14: the InternalRel of A c= the InternalRel of C by A12;

the carrier of A c= the carrier of B by A13, YELLOW_0:def 13;

then the carrier of A c= the carrier of C by A11;

then A is SubRelStr of C by A14, YELLOW_0:def 13;

hence x <= z by Th15; :: thesis: verum

end;reconsider A = x, B = y, C = z as strict SubRelStr of L by Def2;

assume that

A8: x <= y and

A9: y <= z ; :: thesis: x <= z

A10: B is SubRelStr of C by A9, Th15;

then A11: the carrier of B c= the carrier of C by YELLOW_0:def 13;

A12: the InternalRel of B c= the InternalRel of C by A10, YELLOW_0:def 13;

A13: A is SubRelStr of B by A8, Th15;

then the InternalRel of A c= the InternalRel of B by YELLOW_0:def 13;

then A14: the InternalRel of A c= the InternalRel of C by A12;

the carrier of A c= the carrier of B by A13, YELLOW_0:def 13;

then the carrier of A c= the carrier of C by A11;

then A is SubRelStr of C by A14, YELLOW_0:def 13;

hence x <= z by Th15; :: thesis: verum