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 Def2;
A is SubRelStr of A by YELLOW_0:def 13;
hence x <= x by Th15; :: 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 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;
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 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;