set R = Sub L;
thus Sub L is reflexive :: thesis: ( Sub L is antisymmetric & Sub L is transitive )

proof

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 Def3;
A is SubRelStr of A by YELLOW_0:def 13;
hence x <= x by Th16; :: thesis: verum

end;

thus Sub L is antisymmetric :: thesis: Sub L is transitive

proof

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 Def3;
assume that
A1: x <= y and
A2: y <= x ; :: thesis: x = y
A3: B is SubRelStr of A by A2, Th16;
then A4: the carrier of B c= the carrier of A by YELLOW_0:def 13;
A5: A is SubRelStr of B by A1, Th16;
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, XBOOLE_0:def 10;
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;

thus Sub L is transitive :: 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 Def3;
assume that
A8: x <= y and
A9: y <= z ; :: thesis: x <= z
A10: B is SubRelStr of C by A9, Th16;
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, Th16;
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, XBOOLE_1:1;
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, XBOOLE_1:1;
then A is SubRelStr of C by A14, YELLOW_0:def 13;
hence x <= z by Th16; :: thesis: verum

end;