:: deftheorem defines BorrowOutput FSCIRC_1:def 6 :
for x, y, c being set holds BorrowOutput (x,y,c) = [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3];