thus not [.r1,r2,r19,r29.] is empty ; :: thesis: [.r1,r2,r19,r29.] is compact
A1: (LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|)) is compact by COMPTS_1:19;
(LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|)) is compact by COMPTS_1:19;
hence [.r1,r2,r19,r29.] is compact by A1, COMPTS_1:19; :: thesis: verum