theorem :: CARDFIL4:10

for i, j, k, l being Nat st i <= k & j <= l holds
[:(Segm i),(Segm j):] c= [:(Segm k),(Segm l):]