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 ( x <= y & y <= x ) ; :: thesis: x = y
then ( A is SubRelStr of B & B is SubRelStr of A ) by Th16;
then ( the carrier of A c= the carrier of B & the carrier of B c= the carrier of A & the InternalRel of A c= the InternalRel of B & the InternalRel of B c= the InternalRel of A ) by YELLOW_0:def 13;
then ( the carrier of A = the carrier of B & the InternalRel of A = the InternalRel of B ) by XBOOLE_0:def 10;
hence x = y ; :: 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 ( x <= y & y <= z ) ; :: thesis: x <= z
then ( A is SubRelStr of B & B is SubRelStr of C ) by Th16;
then ( the carrier of A c= the carrier of B & the carrier of B c= the carrier of C & the InternalRel of A c= the InternalRel of B & the InternalRel of B c= the InternalRel of C ) by YELLOW_0:def 13;
then ( the carrier of A c= the carrier of C & the InternalRel of A c= the InternalRel of C ) by XBOOLE_1:1;
then A is SubRelStr of C by YELLOW_0:def 13;
hence x <= z by Th16; :: thesis: verum

end;