theorem Th14: :: WAYBEL19:14

for S, T being non empty RelStr
for s being Element of S
for t being Element of T holds (uparrow [s,t]) ` = [:((uparrow s) `), the carrier of T:] \/ [: the carrier of S,((uparrow t) `):]